This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem copsex2g

Description: Implicit substitution inference for ordered pairs. (Contributed by NM, 28-May-1995) Use a similar proof to copsex4g to reduce axiom usage. (Revised by SN, 1-Sep-2024)

Ref Expression
Hypothesis copsex2g.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
Assertion copsex2g ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 copsex2g.1 ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝜑 ↔ 𝜓 ) )
2 eqcom ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
6 2 5 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
7 6 anbi1i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝜑 ) )
8 7 2exbii ⊢ ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝜑 ) )
9 id ⊢ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) → ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
10 9 1 cgsex2g ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∃ 𝑦 ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ 𝜑 ) ↔ 𝜓 ) )
11 8 10 bitrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ∃ 𝑥 ∃ 𝑦 ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ 𝜓 ) )