Metamath Proof Explorer

Theorem brab2a

Description: The law of concretion for a binary relation. Ordered pair membership in an ordered pair class abstraction. (Contributed by Mario Carneiro, 28-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		brab2a.1	$⊢ (x = A \land y = B) \to (φ \leftrightarrow ψ)$
2		brab2a.2	$⊢ R = \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\}$
3		opabssxp	$⊢ \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\} \subseteq C \times D$
4	2 3	eqsstri	$⊢ R \subseteq C \times D$
5	4	brel	$⊢ A R B \to (A \in C \land B \in D)$
6		df-br	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in R$
7	2	eleq2i	$⊢ ⟨A, B⟩ \in R \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\}$
8	6 7	bitri	$⊢ A R B \leftrightarrow ⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\}$
9	1	opelopab2a	$⊢ (A \in C \land B \in D) \to (⟨A, B⟩ \in \{⟨x, y⟩ \| ((x \in C \land y \in D) \land φ)\} \leftrightarrow ψ)$
10	8 9	bitrid	$⊢ (A \in C \land B \in D) \to (A R B \leftrightarrow ψ)$
11	5 10	biadanii	$⊢ A R B \leftrightarrow ((A \in C \land B \in D) \land ψ)$