Metamath Proof Explorer

Theorem copsexgw

Description: Version of copsexg with a disjoint variable condition, which does not require ax-13 . (Contributed by GG, 26-Jan-2024) Shorten proof and remove dependency on ax-10 . (Revised by Eric Schmidt, 2-May-2026)

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

Proof

Step Hyp Ref Expression
1 vex ⊢ 𝑥 ∈ V
2 vex ⊢ 𝑦 ∈ V
3 1 2 eqvinop ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ∃ 𝑧 ∃ 𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
4 19.8a ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5 4 19.8ad ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
6 5 ex ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 → ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
7 vex ⊢ 𝑧 ∈ V
8 vex ⊢ 𝑤 ∈ V
9 7 8 opth ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) )
10 9 anbi1i ⊢ ( ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
11 10 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) )
12 anass ⊢ ( ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
13 12 exbii ⊢ ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
14 19.42v ⊢ ( ∃ 𝑦 ( 𝑧 = 𝑥 ∧ ( 𝑤 = 𝑦 ∧ 𝜑 ) ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
15 13 14 bitri ⊢ ( ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
16 15 exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) ↔ ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
17 ax12ev2c ⊢ ( 𝑧 = 𝑥 → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) )
18 ax12ev2c ⊢ ( 𝑤 = 𝑦 → ( ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) → 𝜑 ) )
19 17 18 sylan9 ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ( 𝑧 = 𝑥 ∧ ∃ 𝑦 ( 𝑤 = 𝑦 ∧ 𝜑 ) ) → 𝜑 ) )
20 16 19 biimtrid ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) ∧ 𝜑 ) → 𝜑 ) )
21 11 20 biimtrid ⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
22 9 21 sylbi ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) → 𝜑 ) )
23 6 22 impbid ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
24 eqeq1 ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) )
25 24 anbi1d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
26 25 2exbidv ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )
27 26 bibi2d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ↔ ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
28 24 27 imbi12d ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ↔ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) ) )
29 23 28 mpbiri ⊢ ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
30 29 adantr ⊢ ( ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
31 30 exlimivv ⊢ ( ∃ 𝑧 ∃ 𝑤 ( 𝐴 = ⟨ 𝑧 , 𝑤 ⟩ ∧ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ) → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
32 3 31 sylbi ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) ) )
33 32 pm2.43i ⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ) )