Metamath Proof Explorer

Theorem ax12v2-o

Description: Rederivation of ax-c15 from ax12v (without using ax-c15 or the full ax-12 ). Thus, the hypothesis ( ax12v ) provides an alternate axiom that can be used in place of ax-c15 . See also axc15 . (Contributed by NM, 2-Feb-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis ax12v2-o.1 ⊢ x = z → φ → ∀ x x = z → φ
Assertion ax12v2-o ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ

Proof

Step Hyp Ref Expression
1 ax12v2-o.1 ⊢ x = z → φ → ∀ x x = z → φ
2 ax6ev ⊢ ∃ z z = y
3 equequ2 ⊢ z = y → x = z ↔ x = y
4 3 adantl ⊢ ¬ ∀ x x = y ∧ z = y → x = z ↔ x = y
5 dveeq2-o ⊢ ¬ ∀ x x = y → z = y → ∀ x z = y
6 5 imp ⊢ ¬ ∀ x x = y ∧ z = y → ∀ x z = y
7 nfa1-o ⊢ Ⅎ x ∀ x z = y
8 3 imbi1d ⊢ z = y → x = z → φ ↔ x = y → φ
9 8 sps-o ⊢ ∀ x z = y → x = z → φ ↔ x = y → φ
10 7 9 albid ⊢ ∀ x z = y → ∀ x x = z → φ ↔ ∀ x x = y → φ
11 6 10 syl ⊢ ¬ ∀ x x = y ∧ z = y → ∀ x x = z → φ ↔ ∀ x x = y → φ
12 11 imbi2d ⊢ ¬ ∀ x x = y ∧ z = y → φ → ∀ x x = z → φ ↔ φ → ∀ x x = y → φ
13 4 12 imbi12d ⊢ ¬ ∀ x x = y ∧ z = y → x = z → φ → ∀ x x = z → φ ↔ x = y → φ → ∀ x x = y → φ
14 1 13 mpbii ⊢ ¬ ∀ x x = y ∧ z = y → x = y → φ → ∀ x x = y → φ
15 14 ex ⊢ ¬ ∀ x x = y → z = y → x = y → φ → ∀ x x = y → φ
16 15 exlimdv ⊢ ¬ ∀ x x = y → ∃ z z = y → x = y → φ → ∀ x x = y → φ
17 2 16 mpi ⊢ ¬ ∀ x x = y → x = y → φ → ∀ x x = y → φ