Theorem ax11b 1224

Description: A bidirectional version of ax-11o 1222.

Assertion

Ref	Expression
ax11b	⊢ ((¬ ∀x x = y ⋀ x = y) → (φ ↔ ∀x(x = y → φ)))

Proof of Theorem ax11b

Step	Hyp	Ref	Expression
1		ax-11o 1222	. . 3 ⊢ (¬ ∀x x = y → (x = y → (φ → ∀x(x = y → φ))))
2	1	imp 350	. 2 ⊢ ((¬ ∀x x = y ⋀ x = y) → (φ → ∀x(x = y → φ)))
3		ax-4 977	. . . 4 ⊢ (∀x(x = y → φ) → (x = y → φ))
4	3	com12 11	. . 3 ⊢ (x = y → (∀x(x = y → φ) → φ))
5	4	adantl 390	. 2 ⊢ ((¬ ∀x x = y ⋀ x = y) → (∀x(x = y → φ) → φ))
6	2, 5	impbid 519	1 ⊢ ((¬ ∀x x = y ⋀ x = y) → (φ ↔ ∀x(x = y → φ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋀ wa 223  ∀wal 958   = wceq 960

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-4 977  ax-11o 1222

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain