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

Metamath Proof Explorer

Theorem copsex4g

Description: An implicit substitution inference for 2 ordered pairs. (Contributed by NM, 5-Aug-1995)

Ref Expression
Hypothesis copsex4g.1 ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) → ( 𝜑 ↔ 𝜓 ) )
Assertion copsex4g ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ∧ 𝜑 ) ↔ 𝜓 ) )

Proof

Step Hyp Ref Expression
1 copsex4g.1 ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) → ( 𝜑 ↔ 𝜓 ) )
2 eqcom ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ )
3 vex ⊢ 𝑥 ∈ V
4 vex ⊢ 𝑦 ∈ V
5 3 4 opth ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝐴 , 𝐵 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
6 2 5 bitri ⊢ ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) )
7 eqcom ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ↔ ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ )
8 vex ⊢ 𝑧 ∈ V
9 vex ⊢ 𝑤 ∈ V
10 8 9 opth ⊢ ( ⟨ 𝑧 , 𝑤 ⟩ = ⟨ 𝐶 , 𝐷 ⟩ ↔ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) )
11 7 10 bitri ⊢ ( ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ↔ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) )
12 6 11 anbi12i ⊢ ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ↔ ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) )
13 12 anbi1i ⊢ ( ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ∧ 𝜑 ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ 𝜑 ) )
14 13 a1i ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆 ) ) → ( ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ∧ 𝜑 ) ↔ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ 𝜑 ) ) )
15 14 4exbidv ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ 𝜑 ) ) )
16 id ⊢ ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) → ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) )
17 16 1 cgsex4g ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ( 𝑥 = 𝐴 ∧ 𝑦 = 𝐵 ) ∧ ( 𝑧 = 𝐶 ∧ 𝑤 = 𝐷 ) ) ∧ 𝜑 ) ↔ 𝜓 ) )
18 15 17 bitrd ⊢ ( ( ( 𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ) ∧ ( 𝐶 ∈ 𝑅 ∧ 𝐷 ∈ 𝑆 ) ) → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ∃ 𝑤 ( ( ⟨ 𝐴 , 𝐵 ⟩ = ⟨ 𝑥 , 𝑦 ⟩ ∧ ⟨ 𝐶 , 𝐷 ⟩ = ⟨ 𝑧 , 𝑤 ⟩ ) ∧ 𝜑 ) ↔ 𝜓 ) )