opelopab2a

Description: Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 19-Dec-2013)

		Ref	Expression
	Hypothesis	opelopabga.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
	Assertion	opelopab2a	$⊢ (A \in C \land B \in D) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\} \leftrightarrow ψ)$

Step	Hyp	Ref	Expression
1		opelopabga.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
2		eleq1	$⊢ x = A \to (x \in C \leftrightarrow A \in C)$
3		eleq1	$⊢ y = B \to (y \in D \leftrightarrow B \in D)$
4	2 3	bi2anan9	$⊢ (x = A \land y = B) \to ((x \in C \land y \in D) \leftrightarrow (A \in C \land B \in D))$
5	4 1	anbi12d	$⊢ (x = A \land y = B) \to (((x \in C \land y \in D) \land φ) \leftrightarrow ((A \in C \land B \in D) \land ψ))$
6	5	opelopabga	$⊢ (A \in C \land B \in D) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\} \leftrightarrow ((A \in C \land B \in D) \land ψ))$
7	6	bianabs	$⊢ (A \in C \land B \in D) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\} \leftrightarrow ψ)$

Metamath Proof Explorer