Metamath Proof Explorer

Theorem 2sb5ndALT

Description: Equivalence for double substitution 2sb5 without distinct x , y requirement. 2sb5nd is derived from 2sb5ndVD . The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in 2sb5ndVD . (Contributed by Alan Sare, 19-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion 2sb5ndALT ⊢ ¬ ∀ x x = y ∨ u = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ

Proof

Step Hyp Ref Expression
1 ax6e2ndeq ⊢ ¬ ∀ x x = y ∨ u = v ↔ ∃ x ∃ y x = u ∧ y = v
2 anabs5 ⊢ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
3 2pm13.193 ⊢ x = u ∧ y = v ∧ u x v y φ ↔ x = u ∧ y = v ∧ φ
4 3 exbii ⊢ ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ y x = u ∧ y = v ∧ φ
5 hbs1 ⊢ u x v y φ → ∀ x u x v y φ
6 id ⊢ ∀ x x = y → ∀ x x = y
7 axc11 ⊢ ∀ x x = y → ∀ x u x v y φ → ∀ y u x v y φ
8 6 7 syl ⊢ ∀ x x = y → ∀ x u x v y φ → ∀ y u x v y φ
9 pm3.33 ⊢ u x v y φ → ∀ x u x v y φ ∧ ∀ x u x v y φ → ∀ y u x v y φ → u x v y φ → ∀ y u x v y φ
10 5 8 9 sylancr ⊢ ∀ x x = y → u x v y φ → ∀ y u x v y φ
11 hbs1 ⊢ v y φ → ∀ y v y φ
12 11 sbt ⊢ u x v y φ → ∀ y v y φ
13 sbi1 ⊢ u x v y φ → ∀ y v y φ → u x v y φ → u x ∀ y v y φ
14 12 13 ax-mp ⊢ u x v y φ → u x ∀ y v y φ
15 id ⊢ ¬ ∀ x x = y → ¬ ∀ x x = y
16 axc11n ⊢ ∀ y y = x → ∀ x x = y
17 16 con3i ⊢ ¬ ∀ x x = y → ¬ ∀ y y = x
18 15 17 syl ⊢ ¬ ∀ x x = y → ¬ ∀ y y = x
19 sbal2 ⊢ ¬ ∀ y y = x → u x ∀ y v y φ ↔ ∀ y u x v y φ
20 18 19 syl ⊢ ¬ ∀ x x = y → u x ∀ y v y φ ↔ ∀ y u x v y φ
21 imbi2 ⊢ u x ∀ y v y φ ↔ ∀ y u x v y φ → u x v y φ → u x ∀ y v y φ ↔ u x v y φ → ∀ y u x v y φ
22 21 biimpac ⊢ u x v y φ → u x ∀ y v y φ ∧ u x ∀ y v y φ ↔ ∀ y u x v y φ → u x v y φ → ∀ y u x v y φ
23 14 20 22 sylancr ⊢ ¬ ∀ x x = y → u x v y φ → ∀ y u x v y φ
24 10 23 pm2.61i ⊢ u x v y φ → ∀ y u x v y φ
25 24 nf5i ⊢ Ⅎ y u x v y φ
26 25 19.41 ⊢ ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ y x = u ∧ y = v ∧ u x v y φ
27 4 26 bitr3i ⊢ ∃ y x = u ∧ y = v ∧ φ ↔ ∃ y x = u ∧ y = v ∧ u x v y φ
28 27 exbii ⊢ ∃ x ∃ y x = u ∧ y = v ∧ φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
29 nfs1v ⊢ Ⅎ x u x v y φ
30 29 19.41 ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ
31 28 30 bitr2i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ
32 31 anbi2i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
33 2 32 bitr3i ⊢ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
34 pm5.32 ⊢ ∃ x ∃ y x = u ∧ y = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ ∃ x ∃ y x = u ∧ y = v ∧ φ
35 33 34 mpbir ⊢ ∃ x ∃ y x = u ∧ y = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ
36 1 35 sylbi ⊢ ¬ ∀ x x = y ∨ u = v → u x v y φ ↔ ∃ x ∃ y x = u ∧ y = v ∧ φ