copsex2gb

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

		Ref	Expression
	Hypothesis	copsex2ga.1	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
	Assertion	copsex2gb	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land ψ) \leftrightarrow (A \in (V \times V) \land φ)$

Step	Hyp	Ref	Expression
1		copsex2ga.1	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
2		elvv	$⊢ A \in (V \times V) \leftrightarrow \exists x \exists y A = ⟨x, y⟩$
3	2	anbi1i	$⊢ (A \in (V \times V) \land φ) \leftrightarrow (\exists x \exists y A = ⟨x, y⟩ \land φ)$
4		19.41vv	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow (\exists x \exists y A = ⟨x, y⟩ \land φ)$
5	1	pm5.32i	$⊢ (A = ⟨x, y⟩ \land φ) \leftrightarrow (A = ⟨x, y⟩ \land ψ)$
6	5	2exbii	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land φ) \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ψ)$
7	3 4 6	3bitr2ri	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land ψ) \leftrightarrow (A \in (V \times V) \land φ)$

Metamath Proof Explorer