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 ( ( ¬ ∀ 𝑥 𝑥 = 𝑦 ∨ 𝑢 = 𝑣 ) → ( [ 𝑢 / 𝑥 ] [ 𝑣 / 𝑦 ] 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝑢 ∧ 𝑦 = 𝑣 ) ∧ 𝜑 ) ) )

Proof

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