opabex3rd

Description: Existence of an ordered pair abstraction if the second components are elements of a set. (Contributed by AV, 17-Sep-2023) (Revised by AV, 9-Aug-2024)

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

Proof

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

Metamath Proof Explorer

Theorem opabex3rd

Proof