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 ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑥𝑦 ) )

Proof

Step Hyp Ref Expression
1 bj-nfeel2 ( ¬ ∀ 𝑧 𝑧 = 𝑥 → Ⅎ 𝑧 𝑥𝑡 )
2 elequ2 ( 𝑡 = 𝑦 → ( 𝑥𝑡𝑥𝑦 ) )
3 1 2 bj-dvelimdv1 ( ¬ ∀ 𝑧 𝑧 = 𝑥 → ( ¬ ∀ 𝑧 𝑧 = 𝑦 → Ⅎ 𝑧 𝑥𝑦 ) )