This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dfopab2

Description: A way to define an ordered-pair class abstraction without using existential quantifiers. (Contributed by NM, 18-Aug-2006) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Assertion	dfopab2	$⊢ \{⟨x, y⟩ \| φ\} = \{z \in (V \times V) \| \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ\}$

Proof

Step	Hyp	Ref	Expression
1		nfsbc1v	$⊢ Ⅎ x \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ$
2	1	19.41	$⊢ \exists x (\exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ) \leftrightarrow (\exists x \exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
3		sbcopeq1a	$⊢ z = ⟨x, y⟩ \to (\underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ \leftrightarrow φ)$
4	3	pm5.32i	$⊢ (z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ) \leftrightarrow (z = ⟨x, y⟩ \land φ)$
5	4	exbii	$⊢ \exists y (z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ) \leftrightarrow \exists y (z = ⟨x, y⟩ \land φ)$
6		nfcv	$⊢ \underline{Ⅎ} y 1^{st} (z)$
7		nfsbc1v	$⊢ Ⅎ y \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ$
8	6 7	nfsbcw	$⊢ Ⅎ y \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ$
9	8	19.41	$⊢ \exists y (z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ) \leftrightarrow (\exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
10	5 9	bitr3i	$⊢ \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow (\exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
11	10	exbii	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow \exists x (\exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
12		elvv	$⊢ z \in (V \times V) \leftrightarrow \exists x \exists y z = ⟨x, y⟩$
13	12	anbi1i	$⊢ (z \in (V \times V) \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ) \leftrightarrow (\exists x \exists y z = ⟨x, y⟩ \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
14	2 11 13	3bitr4i	$⊢ \exists x \exists y (z = ⟨x, y⟩ \land φ) \leftrightarrow (z \in (V \times V) \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)$
15	14	abbii	$⊢ \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\} = \{z \| (z \in (V \times V) \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)\}$
16		df-opab	$⊢ \{⟨x, y⟩ \| φ\} = \{z \| \exists x \exists y (z = ⟨x, y⟩ \land φ)\}$
17		df-rab	$⊢ \{z \in (V \times V) \| \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ\} = \{z \| (z \in (V \times V) \land \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ)\}$
18	15 16 17	3eqtr4i	$⊢ \{⟨x, y⟩ \| φ\} = \{z \in (V \times V) \| \underset{˙}{[} 1^{st} (z) / x \underset{˙}{]} \underset{˙}{[} 2^{nd} (z) / y \underset{˙}{]} φ\}$