Metamath Proof Explorer

Theorem inopab

Description: Intersection of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

		Ref	Expression
	Assertion	inopab	$⊢ \{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		relopabv	$⊢ Rel \{⟨x, y⟩ \| φ\}$
2		relin1	$⊢ Rel \{⟨x, y⟩ \| φ\} \to Rel (\{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\})$
3	1 2	ax-mp	$⊢ Rel (\{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\})$
4		relopabv	$⊢ Rel \{⟨x, y⟩ \| (φ \land ψ)\}$
5		sban	$⊢ [z/ x] ([w/ y] φ \land [w/ y] ψ) \leftrightarrow ([z/ x] [w/ y] φ \land [z/ x] [w/ y] ψ)$
6		sban	$⊢ [w/ y] (φ \land ψ) \leftrightarrow ([w/ y] φ \land [w/ y] ψ)$
7	6	sbbii	$⊢ [z/ x] [w/ y] (φ \land ψ) \leftrightarrow [z/ x] ([w/ y] φ \land [w/ y] ψ)$
8		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \leftrightarrow [z/ x] [w/ y] φ$
9		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\} \leftrightarrow [z/ x] [w/ y] ψ$
10	8 9	anbi12i	$⊢ (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\}) \leftrightarrow ([z/ x] [w/ y] φ \land [z/ x] [w/ y] ψ)$
11	5 7 10	3bitr4ri	$⊢ (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\}) \leftrightarrow [z/ x] [w/ y] (φ \land ψ)$
12		elin	$⊢ ⟨z, w⟩ \in (\{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\}) \leftrightarrow (⟨z, w⟩ \in \{⟨x, y⟩ \| φ\} \land ⟨z, w⟩ \in \{⟨x, y⟩ \| ψ\})$
13		vopelopabsb	$⊢ ⟨z, w⟩ \in \{⟨x, y⟩ \| (φ \land ψ)\} \leftrightarrow [z/ x] [w/ y] (φ \land ψ)$
14	11 12 13	3bitr4i	$⊢ ⟨z, w⟩ \in (\{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\}) \leftrightarrow ⟨z, w⟩ \in \{⟨x, y⟩ \| (φ \land ψ)\}$
15	3 4 14	eqrelriiv	$⊢ \{⟨x, y⟩ \| φ\} \cap \{⟨x, y⟩ \| ψ\} = \{⟨x, y⟩ \| (φ \land ψ)\}$