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→φ→∀xx=z→φ
Assertion ax12v2-o ⊢¬∀xx=y→x=y→φ→∀xx=y→φ

Proof

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