Metamath Proof Explorer


Theorem bj-axc14nf

Description: Proof of a version of axc14 using the "nonfree" idiom. (Contributed by BJ, 20-Oct-2021) (Proof modification is discouraged.)

Ref Expression
Assertion bj-axc14nf ¬ z z = x ¬ z z = y z x y

Proof

Step Hyp Ref Expression
1 bj-nfeel2 ¬ z z = x z x t
2 elequ2 t = y x t x y
3 1 2 bj-dvelimdv1 ¬ z z = x ¬ z z = y z x y