Theorem axc16nfALT

Alternate proof of axc16nf, shorter but requiring [ax-11] and [ax-13]. (Contributed by Mario Carneiro, 7-Oct-2016.) (Proof modification is discouraged.) (New usage is discouraged.)

Conclusion
\( \vdash \forall x \, x = y \rightarrow \Finv z \, \varphi \)
Proof
l0
nfae
axc16g
nf5d l0 _