Metamath Proof Explorer

Theorem dfoprab4

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 3-Sep-2007) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	dfoprab4.1	$⊢ w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
	Assertion	dfoprab4	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$

Proof

Step	Hyp	Ref	Expression
1		dfoprab4.1	$⊢ w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
2		xpss	$⊢ A \times B \subseteq V \times V$
3	2	sseli	$⊢ w \in (A \times B) \to w \in (V \times V)$
4	3	adantr	$⊢ (w \in (A \times B) \land φ) \to w \in (V \times V)$
5	4	pm4.71ri	$⊢ (w \in (A \times B) \land φ) \leftrightarrow (w \in (V \times V) \land (w \in (A \times B) \land φ))$
6	5	opabbii	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨w, z⟩ \| (w \in (V \times V) \land (w \in (A \times B) \land φ))\}$
7		eleq1	$⊢ w = ⟨x, y⟩ \to (w \in (A \times B) \leftrightarrow ⟨x, y⟩ \in (A \times B))$
8		opelxp	$⊢ ⟨x, y⟩ \in (A \times B) \leftrightarrow (x \in A \land y \in B)$
9	7 8	bitrdi	$⊢ w = ⟨x, y⟩ \to (w \in (A \times B) \leftrightarrow (x \in A \land y \in B))$
10	9 1	anbi12d	$⊢ w = ⟨x, y⟩ \to ((w \in (A \times B) \land φ) \leftrightarrow ((x \in A \land y \in B) \land ψ))$
11	10	dfoprab3	$⊢ \{⟨w, z⟩ \| (w \in (V \times V) \land (w \in (A \times B) \land φ))\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$
12	6 11	eqtri	$⊢ \{⟨w, z⟩ \| (w \in (A \times B) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ((x \in A \land y \in B) \land ψ)\}$