Theorem bj-hbnaeb 36573

Description: Biconditional version of hbnae 2429 (to replace it?). (Contributed by BJ, 6-Oct-2018.)

Assertion

Ref	Expression
bj-hbnaeb	⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)

Proof of Theorem bj-hbnaeb

Step	Hyp	Ref	Expression
1		hbnae 2429	. 2 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 → ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)
2		sp 2175	. 2 ⊢ (∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦 → ¬ ∀𝑥 𝑥 = 𝑦)
3	1, 2	impbii 208	1 ⊢ (¬ ∀𝑥 𝑥 = 𝑦 ↔ ∀𝑧 ¬ ∀𝑥 𝑥 = 𝑦)

Syntax hints:  ¬ wn 3   ↔ wb 205  ∀wal 1532

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-10 2133  ax-11 2150  ax-12 2170  ax-13 2369

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-tru 1537  df-ex 1775  df-nf 1779

This theorem is referenced by: (None)