Theorem relopabVD 43173

Description: Virtual deduction proof of relopab 5780. The following User's Proof is a Virtual Deduction proof completed automatically by the tools program completeusersproof.cmd, which invokes Mel L. O'Cat's mmj2 and Norm Megill's Metamath Proof Assistant. relopab 5780 is relopabVD 43173 without virtual deductions and was automatically derived from relopabVD 43173.

1::	⊢ (   𝑦 = 𝑣   ▶   𝑦 = 𝑣   )
2:1:	⊢ (   𝑦 = 𝑣   ▶   ⟨𝑥   ,   𝑦⟩ = ⟨𝑥   ,   𝑣 ⟩   )
3::	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
4:3:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥   ,   𝑣⟩ = ⟨ 𝑢, 𝑣⟩   )
5:2,4:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥   ,   𝑦⟩ = ⟨ 𝑢, 𝑣⟩   )
6:5:	⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   (𝑧 = ⟨𝑥   ,   𝑦 ⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)   )
7:6:	⊢ (   𝑦 = 𝑣   ▶   (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,    𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))   )
8:7:	⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦 ⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
9:8:	⊢ (∃𝑣𝑦 = 𝑣 → ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
90::	⊢ (𝑣 = 𝑦 ↔ 𝑦 = 𝑣)
91:90:	⊢ (∃𝑣𝑣 = 𝑦 ↔ ∃𝑣𝑦 = 𝑣)
92::	⊢ ∃𝑣𝑣 = 𝑦
10:91,92:	⊢ ∃𝑣𝑦 = 𝑣
11:9,10:	⊢ ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
12:11:	⊢ (𝑥 = 𝑢 → ∃𝑣(𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
13::	⊢ (∃𝑣(𝑧 = ⟨𝑥   ,   𝑦⟩ → 𝑧 = ⟨𝑢 , 𝑣⟩) → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩))
14:12,13:	⊢ (𝑥 = 𝑢 → (𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
15:14:	⊢ (∃𝑢𝑥 = 𝑢 → ∃𝑢(𝑧 = ⟨𝑥   ,   𝑦 ⟩ → ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩))
150::	⊢ (𝑢 = 𝑥 ↔ 𝑥 = 𝑢)
151:150:	⊢ (∃𝑢𝑢 = 𝑥 ↔ ∃𝑢𝑥 = 𝑢)
152::	⊢ ∃𝑢𝑢 = 𝑥
16:151,152:	⊢ ∃𝑢𝑥 = 𝑢
17:15,16:	⊢ ∃𝑢(𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑣𝑧 = ⟨ 𝑢, 𝑣⟩)
18:17:	⊢ (𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢∃𝑣𝑧 = ⟨ 𝑢, 𝑣⟩)
19:18:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑦∃𝑢 ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
20::	⊢ (∃𝑦∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
21:19,20:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
22:21:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑥 ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
23::	⊢ (∃𝑥∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ → ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
24:22,23:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ → ∃𝑢 ∃𝑣𝑧 = ⟨𝑢, 𝑣⟩)
25:24:	⊢ {𝑧 ∣ ∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩} ⊆ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩}
26::	⊢ 𝑥 ∈ V
27::	⊢ 𝑦 ∈ V
28:26,27:	⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
29:28:	⊢ (𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ (𝑧 = ⟨𝑥   ,   𝑦 ⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
30:29:	⊢ (∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
31:30:	⊢ (∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩ ↔ ∃𝑥 ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
32:31:	⊢ {𝑧 ∣ ∃𝑥∃𝑦𝑧 = ⟨𝑥   ,   𝑦⟩} = { 𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
320:25,32:	⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥   ,   𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢, 𝑣⟩}
33::	⊢ 𝑢 ∈ V
34::	⊢ 𝑣 ∈ V
35:33,34:	⊢ (𝑢 ∈ V ∧ 𝑣 ∈ V)
36:35:	⊢ (𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ (𝑧 = ⟨𝑢   ,   𝑣 ⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
37:36:	⊢ (∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
38:37:	⊢ (∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩ ↔ ∃𝑢 ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
39:38:	⊢ {𝑧 ∣ ∃𝑢∃𝑣𝑧 = ⟨𝑢   ,   𝑣⟩} = { 𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
40:320,39:	⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥   ,   𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
41::	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)) }
42::	⊢ {⟨𝑢   ,   𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V )} = {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) }
43:40,41,42:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
44::	⊢ {⟨𝑢   ,   𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V )} = (V × V)
45:43,44:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V )} ⊆ (V × V)
46:28:	⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
47:46:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥   ,   𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
48:45,47:	⊢ {⟨𝑥   ,   𝑦⟩ ∣ 𝜑} ⊆ (V × V)
qed:48:	⊢ Rel {⟨𝑥   ,   𝑦⟩ ∣ 𝜑}

(Contributed by Alan Sare, 9-Jul-2013.) (Proof modification is discouraged.) (New usage is discouraged.)

Assertion

Ref	Expression
relopabVD	⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Proof of Theorem relopabVD

Dummy variables 𝑧 𝑣 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 3449	. . . . . 6 ⊢ 𝑥 ∈ V
2		vex 3449	. . . . . 6 ⊢ 𝑦 ∈ V
3	1, 2	pm3.2i 471	. . . . 5 ⊢ (𝑥 ∈ V ∧ 𝑦 ∈ V)
4	3	a1i 11	. . . 4 ⊢ (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
5	4	ssopab2i 5507	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
6	3	biantru 530	. . . . . . . . . 10 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
7	6	exbii 1850	. . . . . . . . 9 ⊢ (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
8	7	exbii 1850	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
9	8	abbii 2806	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
10		ax6ev 1973	. . . . . . . . . . . . . . 15 ⊢ ∃𝑢 𝑢 = 𝑥
11		equcom 2021	. . . . . . . . . . . . . . . 16 ⊢ (𝑢 = 𝑥 ↔ 𝑥 = 𝑢)
12	11	exbii 1850	. . . . . . . . . . . . . . 15 ⊢ (∃𝑢 𝑢 = 𝑥 ↔ ∃𝑢 𝑥 = 𝑢)
13	10, 12	mpbi 229	. . . . . . . . . . . . . 14 ⊢ ∃𝑢 𝑥 = 𝑢
14		ax6ev 1973	. . . . . . . . . . . . . . . . . . 19 ⊢ ∃𝑣 𝑣 = 𝑦
15		equcom 2021	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑣 = 𝑦 ↔ 𝑦 = 𝑣)
16	15	exbii 1850	. . . . . . . . . . . . . . . . . . 19 ⊢ (∃𝑣 𝑣 = 𝑦 ↔ ∃𝑣 𝑦 = 𝑣)
17	14, 16	mpbi 229	. . . . . . . . . . . . . . . . . 18 ⊢ ∃𝑣 𝑦 = 𝑣
18		idn1 42846	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (   𝑦 = 𝑣   ▶   𝑦 = 𝑣   )
19		opeq2 4831	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
20	18, 19	e1a 42899	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (   𝑦 = 𝑣   ▶   ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩   )
21		idn2 42885	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
22		opeq1 4830	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
23	21, 22	e2 42903	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩   )
24		eqeq1 2740	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ ↔ ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩))
25	24	biimprd 247	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩ → ⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩))
26	20, 23, 25	e12 42996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   ⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩   )
27		eqeq2 2748	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑢, 𝑣⟩))
28	27	biimpd 228	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
29	26, 28	e2 42903	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)   )
30	29	in2 42877	. . . . . . . . . . . . . . . . . . . 20 ⊢ (   𝑦 = 𝑣   ▶   (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))   )
31	30	in1 42843	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
32	31	eximi 1837	. . . . . . . . . . . . . . . . . 18 ⊢ (∃𝑣 𝑦 = 𝑣 → ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
33	17, 32	ax-mp 5	. . . . . . . . . . . . . . . . 17 ⊢ ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
34	33	19.37iv 1952	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 𝑢 → ∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
35		19.37v 1995	. . . . . . . . . . . . . . . . 17 ⊢ (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
36	35	biimpi 215	. . . . . . . . . . . . . . . 16 ⊢ (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
37	34, 36	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
38	37	eximi 1837	. . . . . . . . . . . . . 14 ⊢ (∃𝑢 𝑥 = 𝑢 → ∃𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
39	13, 38	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ∃𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
40	39	19.37iv 1952	. . . . . . . . . . . 12 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
41	40	eximi 1837	. . . . . . . . . . 11 ⊢ (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
42		19.9v 1987	. . . . . . . . . . . 12 ⊢ (∃𝑦∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
43	42	biimpi 215	. . . . . . . . . . 11 ⊢ (∃𝑦∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
44	41, 43	syl 17	. . . . . . . . . 10 ⊢ (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
45	44	eximi 1837	. . . . . . . . 9 ⊢ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
46		19.9v 1987	. . . . . . . . . 10 ⊢ (∃𝑥∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
47	46	biimpi 215	. . . . . . . . 9 ⊢ (∃𝑥∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
48	45, 47	syl 17	. . . . . . . 8 ⊢ (∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
49	48	ss2abi 4023	. . . . . . 7 ⊢ {𝑧 ∣ ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩} ⊆ {𝑧 ∣ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
50	9, 49	eqsstrri 3979	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
51		vex 3449	. . . . . . . . . . 11 ⊢ 𝑢 ∈ V
52		vex 3449	. . . . . . . . . . 11 ⊢ 𝑣 ∈ V
53	51, 52	pm3.2i 471	. . . . . . . . . 10 ⊢ (𝑢 ∈ V ∧ 𝑣 ∈ V)
54	53	biantru 530	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑢, 𝑣⟩ ↔ (𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
55	54	exbii 1850	. . . . . . . 8 ⊢ (∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
56	55	exbii 1850	. . . . . . 7 ⊢ (∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
57	56	abbii 2806	. . . . . 6 ⊢ {𝑧 ∣ ∃𝑢∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩} = {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
58	50, 57	sseqtri 3980	. . . . 5 ⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
59		df-opab 5168	. . . . 5 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
60		df-opab 5168	. . . . 5 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = {𝑧 ∣ ∃𝑢∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
61	58, 59, 60	3sstr4i 3987	. . . 4 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
62		df-xp 5639	. . . . 5 ⊢ (V × V) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
63	62	eqcomi 2745	. . . 4 ⊢ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = (V × V)
64	61, 63	sseqtri 3980	. . 3 ⊢ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ (V × V)
65	5, 64	sstri 3953	. 2 ⊢ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V)
66		df-rel 5640	. . 3 ⊢ (Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V))
67	66	biimpri 227	. 2 ⊢ ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V) → Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑})
68	65, 67	e0a 43044	1 ⊢ Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  {cab 2713  Vcvv 3445   ⊆ wss 3910  ⟨cop 4592  {copab 5167   × cxp 5631  Rel wrel 5638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3408  df-v 3447  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-opab 5168  df-xp 5639  df-rel 5640  df-vd1 42842  df-vd2 42850

This theorem is referenced by: (None)