Theorem copsex2gb

Description: Implicit substitution inference for ordered pairs. Compare copsex2ga . (Contributed by NM, 12-Mar-2014)

	Ref	Expression
Hypothesis	copsex2ga.1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
Assertion	copsex2gb	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) )

Proof

Step	Hyp	Ref	Expression
1		copsex2ga.1	⊢ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ → ( 𝜑 ↔ 𝜓 ) )
2		elvv	⊢ ( 𝐴 ∈ ( V × V ) ↔ ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ )
3	2	anbi1i	⊢ ( ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
4		19.41vv	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( ∃ 𝑥 ∃ 𝑦 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) )
5	1	pm5.32i	⊢ ( ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
6	5	2exbii	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) )
7	3 4 6	3bitr2ri	⊢ ( ∃ 𝑥 ∃ 𝑦 ( 𝐴 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ↔ ( 𝐴 ∈ ( V × V ) ∧ 𝜑 ) )