Metamath Proof Explorer

Theorem copsex2ga

Description: Implicit substitution inference for ordered pairs. Compare copsex2g . (Contributed by NM, 26-Feb-2014) (Proof shortened by Mario Carneiro, 31-Aug-2015)

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

Proof

Step	Hyp	Ref	Expression
1		copsex2ga.1	$⊢ A = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
2		xpss	$⊢ V \times W \subseteq V \times V$
3	2	sseli	$⊢ A \in (V \times W) \to A \in (V \times V)$
4	1	copsex2gb	$⊢ \exists x \exists y (A = ⟨x, y⟩ \land ψ) \leftrightarrow (A \in (V \times V) \land φ)$
5	4	baibr	$⊢ A \in (V \times V) \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ψ))$
6	3 5	syl	$⊢ A \in (V \times W) \to (φ \leftrightarrow \exists x \exists y (A = ⟨x, y⟩ \land ψ))$