opabex3

Description: Existence of an ordered pair abstraction. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Hypotheses	opabex3.1	$⊢ A \in V$
	opabex3.2	$⊢ x \in A \to \{y \| φ\} \in V$
Assertion	opabex3	$⊢ \{⟨x, y⟩ \| (x \in A \land φ)\} \in V$

Proof

Step	Hyp	Ref	Expression
1		opabex3.1	$⊢ A \in V$
2		opabex3.2	$⊢ x \in A \to \{y \| φ\} \in V$
3		19.42v	$⊢ \exists y (x \in A \land (z = ⟨x, y⟩ \land φ)) \leftrightarrow (x \in A \land \exists y (z = ⟨x, y⟩ \land φ))$
4		an12	$⊢ (z = ⟨x, y⟩ \land (x \in A \land φ)) \leftrightarrow (x \in A \land (z = ⟨x, y⟩ \land φ))$
5	4	exbii	$⊢ \exists y (z = ⟨x, y⟩ \land (x \in A \land φ)) \leftrightarrow \exists y (x \in A \land (z = ⟨x, y⟩ \land φ))$
6		elxp	$⊢ z \in (\{x\} \times \{y \| φ\}) \leftrightarrow \exists v \exists w (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\}))$
7		excom	$⊢ \exists v \exists w (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow \exists w \exists v (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\}))$
8		an12	$⊢ (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow (v \in \{x\} \land (z = ⟨v, w⟩ \land w \in \{y \| φ\}))$
9		velsn	$⊢ v \in \{x\} \leftrightarrow v = x$
10	9	anbi1i	$⊢ (v \in \{x\} \land (z = ⟨v, w⟩ \land w \in \{y \| φ\})) \leftrightarrow (v = x \land (z = ⟨v, w⟩ \land w \in \{y \| φ\}))$
11	8 10	bitri	$⊢ (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow (v = x \land (z = ⟨v, w⟩ \land w \in \{y \| φ\}))$
12	11	exbii	$⊢ \exists v (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow \exists v (v = x \land (z = ⟨v, w⟩ \land w \in \{y \| φ\}))$
13		opeq1	$⊢ v = x \to ⟨v, w⟩ = ⟨x, w⟩$
14	13	eqeq2d	$⊢ v = x \to (z = ⟨v, w⟩ \leftrightarrow z = ⟨x, w⟩)$
15	14	anbi1d	$⊢ v = x \to ((z = ⟨v, w⟩ \land w \in \{y \| φ\}) \leftrightarrow (z = ⟨x, w⟩ \land w \in \{y \| φ\}))$
16	15	equsexvw	$⊢ \exists v (v = x \land (z = ⟨v, w⟩ \land w \in \{y \| φ\})) \leftrightarrow (z = ⟨x, w⟩ \land w \in \{y \| φ\})$
17	12 16	bitri	$⊢ \exists v (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow (z = ⟨x, w⟩ \land w \in \{y \| φ\})$
18	17	exbii	$⊢ \exists w \exists v (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow \exists w (z = ⟨x, w⟩ \land w \in \{y \| φ\})$
19	7 18	bitri	$⊢ \exists v \exists w (z = ⟨v, w⟩ \land (v \in \{x\} \land w \in \{y \| φ\})) \leftrightarrow \exists w (z = ⟨x, w⟩ \land w \in \{y \| φ\})$
20		nfv	$⊢ Ⅎ y z = ⟨x, w⟩$
21		nfsab1	$⊢ Ⅎ y w \in \{y \| φ\}$
22	20 21	nfan	$⊢ Ⅎ y (z = ⟨x, w⟩ \land w \in \{y \| φ\})$
23		nfv	$⊢ Ⅎ w (z = ⟨x, y⟩ \land φ)$
24		opeq2	$⊢ w = y \to ⟨x, w⟩ = ⟨x, y⟩$
25	24	eqeq2d	$⊢ w = y \to (z = ⟨x, w⟩ \leftrightarrow z = ⟨x, y⟩)$
26		sbequ12	$⊢ y = w \to (φ \leftrightarrow [w/ y] φ)$
27	26	equcoms	$⊢ w = y \to (φ \leftrightarrow [w/ y] φ)$
28		df-clab	$⊢ w \in \{y \| φ\} \leftrightarrow [w/ y] φ$
29	27 28	syl6rbbr	$⊢ w = y \to (w \in \{y \| φ\} \leftrightarrow φ)$
30	25 29	anbi12d	$⊢ w = y \to ((z = ⟨x, w⟩ \land w \in \{y \| φ\}) \leftrightarrow (z = ⟨x, y⟩ \land φ))$
31	22 23 30	cbvexv1	$⊢ \exists w (z = ⟨x, w⟩ \land w \in \{y \| φ\}) \leftrightarrow \exists y (z = ⟨x, y⟩ \land φ)$
32	6 19 31	3bitri	$⊢ z \in (\{x\} \times \{y \| φ\}) \leftrightarrow \exists y (z = ⟨x, y⟩ \land φ)$
33	32	anbi2i	$⊢ (x \in A \land z \in (\{x\} \times \{y \| φ\})) \leftrightarrow (x \in A \land \exists y (z = ⟨x, y⟩ \land φ))$
34	3 5 33	3bitr4ri	$⊢ (x \in A \land z \in (\{x\} \times \{y \| φ\})) \leftrightarrow \exists y (z = ⟨x, y⟩ \land (x \in A \land φ))$
35	34	exbii	$⊢ \exists x (x \in A \land z \in (\{x\} \times \{y \| φ\})) \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land φ))$
36		eliun	$⊢ z \in ⋃_{x \in A} (\{x\} \times \{y \| φ\}) \leftrightarrow \exists x \in A z \in (\{x\} \times \{y \| φ\})$
37		df-rex	$⊢ \exists x \in A z \in (\{x\} \times \{y \| φ\}) \leftrightarrow \exists x (x \in A \land z \in (\{x\} \times \{y \| φ\}))$
38	36 37	bitri	$⊢ z \in ⋃_{x \in A} (\{x\} \times \{y \| φ\}) \leftrightarrow \exists x (x \in A \land z \in (\{x\} \times \{y \| φ\}))$
39		elopab	$⊢ z \in \{⟨x, y⟩ \| (x \in A \land φ)\} \leftrightarrow \exists x \exists y (z = ⟨x, y⟩ \land (x \in A \land φ))$
40	35 38 39	3bitr4i	$⊢ z \in ⋃_{x \in A} (\{x\} \times \{y \| φ\}) \leftrightarrow z \in \{⟨x, y⟩ \| (x \in A \land φ)\}$
41	40	eqriv	$⊢ ⋃_{x \in A} (\{x\} \times \{y \| φ\}) = \{⟨x, y⟩ \| (x \in A \land φ)\}$
42		snex	$⊢ \{x\} \in V$
43		xpexg	$⊢ (\{x\} \in V \land \{y \| φ\} \in V) \to \{x\} \times \{y \| φ\} \in V$
44	42 2 43	sylancr	$⊢ x \in A \to \{x\} \times \{y \| φ\} \in V$
45	44	rgen	$⊢ \forall x \in A \{x\} \times \{y \| φ\} \in V$
46		iunexg	$⊢ (A \in V \land \forall x \in A \{x\} \times \{y \| φ\} \in V) \to ⋃_{x \in A} (\{x\} \times \{y \| φ\}) \in V$
47	1 45 46	mp2an	$⊢ ⋃_{x \in A} (\{x\} \times \{y \| φ\}) \in V$
48	41 47	eqeltrri	$⊢ \{⟨x, y⟩ \| (x \in A \land φ)\} \in V$

Metamath Proof Explorer

Theorem opabex3

Proof