Metamath Proof Explorer

Theorem dfoprab3

Description: Operation class abstraction expressed without existential quantifiers. (Contributed by NM, 16-Dec-2008)

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

Proof

Step	Hyp	Ref	Expression
1		dfoprab3.1	$⊢ w = ⟨x, y⟩ \to (φ \leftrightarrow ψ)$
2		dfoprab3s	$⊢ \{⟨⟨x, y⟩, z⟩ \| ψ\} = \{⟨w, z⟩ \| (w \in (V \times V) \land \underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} ψ)\}$
3		fvex	$⊢ 1^{st} (w) \in V$
4		fvex	$⊢ 2^{nd} (w) \in V$
5		eqcom	$⊢ x = 1^{st} (w) \leftrightarrow 1^{st} (w) = x$
6		eqcom	$⊢ y = 2^{nd} (w) \leftrightarrow 2^{nd} (w) = y$
7	5 6	anbi12i	$⊢ (x = 1^{st} (w) \land y = 2^{nd} (w)) \leftrightarrow (1^{st} (w) = x \land 2^{nd} (w) = y)$
8		eqopi	$⊢ (w \in (V \times V) \land (1^{st} (w) = x \land 2^{nd} (w) = y)) \to w = ⟨x, y⟩$
9	7 8	sylan2b	$⊢ (w \in (V \times V) \land (x = 1^{st} (w) \land y = 2^{nd} (w))) \to w = ⟨x, y⟩$
10	9 1	syl	$⊢ (w \in (V \times V) \land (x = 1^{st} (w) \land y = 2^{nd} (w))) \to (φ \leftrightarrow ψ)$
11	10	bicomd	$⊢ (w \in (V \times V) \land (x = 1^{st} (w) \land y = 2^{nd} (w))) \to (ψ \leftrightarrow φ)$
12	11	ex	$⊢ w \in (V \times V) \to ((x = 1^{st} (w) \land y = 2^{nd} (w)) \to (ψ \leftrightarrow φ))$
13	3 4 12	sbc2iedv	$⊢ w \in (V \times V) \to (\underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} ψ \leftrightarrow φ)$
14	13	pm5.32i	$⊢ (w \in (V \times V) \land \underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} ψ) \leftrightarrow (w \in (V \times V) \land φ)$
15	14	opabbii	$⊢ \{⟨w, z⟩ \| (w \in (V \times V) \land \underset{˙}{[} 1^{st} (w) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (w) / y \underset{˙}{]} ψ)\} = \{⟨w, z⟩ \| (w \in (V \times V) \land φ)\}$
16	2 15	eqtr2i	$⊢ \{⟨w, z⟩ \| (w \in (V \times V) \land φ)\} = \{⟨⟨x, y⟩, z⟩ \| ψ\}$