opabex3d

Description: Existence of an ordered pair abstraction, deduction version. (Contributed by Alexander van der Vekens, 19-Oct-2017) (Revised by AV, 9-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		opabex3d.1	$⊢ φ \to A \in V$
2		opabex3d.2	$⊢ (φ \land 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		df-clab	$⊢ w \in \{y \| ψ\} \leftrightarrow [w/ y] ψ$
27		sbequ12	$⊢ y = w \to (ψ \leftrightarrow [w/ y] ψ)$
28	27	equcoms	$⊢ w = y \to (ψ \leftrightarrow [w/ y] ψ)$
29	26 28	bitr4id	$⊢ 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		vsnex	$⊢ \{x\} \in V$
43		xpexg	$⊢ (\{x\} \in V \land \{y \| ψ\} \in V) \to \{x\} \times \{y \| ψ\} \in V$
44	42 2 43	sylancr	$⊢ (φ \land x \in A) \to \{x\} \times \{y \| ψ\} \in V$
45	44	ralrimiva	$⊢ φ \to \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	syl2anc	$⊢ φ \to ⋃_{x \in A} (\{x\} \times \{y \| ψ\}) \in V$
48	41 47	eqeltrrid	$⊢ φ \to \{⟨x, y⟩ \| (x \in A \land ψ)\} \in V$

Metamath Proof Explorer

Theorem opabex3d

Proof