Metamath Proof Explorer

Theorem copsexg

Description: Substitution of class A for ordered pair <. x , y >. . Usage of this theorem is discouraged because it depends on ax-13 . Use the weaker copsexgw when possible. (Contributed by NM, 27-Dec-1996) (Revised by Andrew Salmon, 11-Jul-2011) (Proof shortened by Wolf Lammen, 25-Aug-2019) (New usage is discouraged.)

Ref Expression
Assertion copsexg ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 1 2 eqvinop ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
4 19.8a ⊢ ( ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5 4 19.23bi ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
6 5 ex ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
7 vex ⊢ 𝑧 ∈ V
8 vex ⊢ 𝑤 ∈ V
9 7 8 opth ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
10 9 anbi1i ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
11 10 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
12 nfe1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) )
13 19.8a ⊢ ( ( 𝑤 = 𝑦 ∧ 𝜑 ) → ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) )
14 13 anim2i ⊢ ( ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
15 14 anassrs ⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
16 15 eximi ⊢ ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
17 biidd ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
18 17 drex1 ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ↔ ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
19 16 18 imbitrid ⊢ ( ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
20 anass ⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
21 20 exbii ⊢ ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
22 19.40 ⊢ ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ( ∃ 𝑦 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
23 nfeqf2 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → Ⅎ 𝑦 𝑧 = 𝑥 )
24 23 19.9d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 𝑧 = 𝑥 → 𝑧 = 𝑥 ) )
25 24 anim1d ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ( ∃ 𝑦 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
26 22 25 syl5 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
27 21 26 biimtrid ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
28 19.8a ⊢ ( ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
29 27 28 syl6 ⊢ ( ¬ ∀ 𝑦 𝑦 = 𝑥 → ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ) )
30 19 29 pm2.61i ⊢ ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
31 12 30 exlimi ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
32 ax12ev2c ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
33 ax12ev2c ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) → 𝜑 ) )
34 32 33 sylan9 ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → 𝜑 ) )
35 31 34 syl5 ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → 𝜑 ) )
36 11 35 biimtrid ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
37 9 36 sylbi ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
38 6 37 impbid ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
39 eqeq1 ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
40 39 anbi1d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
41 40 2exbidv ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
42 41 bibi2d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
43 39 42 imbi12d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ) )
44 38 43 mpbiri ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
45 44 adantr ⊢ ( ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
46 45 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
47 3 46 sylbi ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
48 47 pm2.43i ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )