Users' Mathboxes Mathbox for Alan Sare < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  relopabVD Structured version   Visualization version   GIF version

Theorem relopabVD 44482
Description: Virtual deduction proof of relopab 5826. 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 5826 is relopabVD 44482 without virtual deductions and was automatically derived from relopabVD 44482.
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.
StepHypRef Expression
1 vex 3465 . . . . . 6 𝑥 ∈ V
2 vex 3465 . . . . . 6 𝑦 ∈ V
31, 2pm3.2i 469 . . . . 5 (𝑥 ∈ V ∧ 𝑦 ∈ V)
43a1i 11 . . . 4 (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
54ssopab2i 5552 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
63biantru 528 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
76exbii 1842 . . . . . . . . 9 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
87exbii 1842 . . . . . . . 8 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
98abbii 2795 . . . . . . 7 {𝑧 ∣ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
10 ax6ev 1965 . . . . . . . . . . . . . . 15 𝑢 𝑢 = 𝑥
11 equcom 2013 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥𝑥 = 𝑢)
1211exbii 1842 . . . . . . . . . . . . . . 15 (∃𝑢 𝑢 = 𝑥 ↔ ∃𝑢 𝑥 = 𝑢)
1310, 12mpbi 229 . . . . . . . . . . . . . 14 𝑢 𝑥 = 𝑢
14 ax6ev 1965 . . . . . . . . . . . . . . . . . . 19 𝑣 𝑣 = 𝑦
15 equcom 2013 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑦𝑦 = 𝑣)
1615exbii 1842 . . . . . . . . . . . . . . . . . . 19 (∃𝑣 𝑣 = 𝑦 ↔ ∃𝑣 𝑦 = 𝑣)
1714, 16mpbi 229 . . . . . . . . . . . . . . . . . 18 𝑣 𝑦 = 𝑣
18 idn1 44155 . . . . . . . . . . . . . . . . . . . . . . . 24 (   𝑦 = 𝑣   ▶   𝑦 = 𝑣   )
19 opeq2 4876 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
2018, 19e1a 44208 . . . . . . . . . . . . . . . . . . . . . . 23 (   𝑦 = 𝑣   ▶   𝑥, 𝑦⟩ = ⟨𝑥, 𝑣   )
21 idn2 44194 . . . . . . . . . . . . . . . . . . . . . . . 24 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
22 opeq1 4875 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
2321, 22e2 44212 . . . . . . . . . . . . . . . . . . . . . . 23 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥, 𝑣⟩ = ⟨𝑢, 𝑣   )
24 eqeq1 2729 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ ↔ ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩))
2524biimprd 247 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩ → ⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩))
2620, 23, 25e12 44305 . . . . . . . . . . . . . . . . . . . . . 22 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥, 𝑦⟩ = ⟨𝑢, 𝑣   )
27 eqeq2 2737 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑢, 𝑣⟩))
2827biimpd 228 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
2926, 28e2 44212 . . . . . . . . . . . . . . . . . . . . 21 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)   )
3029in2 44186 . . . . . . . . . . . . . . . . . . . 20 (   𝑦 = 𝑣   ▶   (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))   )
3130in1 44152 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
3231eximi 1829 . . . . . . . . . . . . . . . . . 18 (∃𝑣 𝑦 = 𝑣 → ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
3317, 32ax-mp 5 . . . . . . . . . . . . . . . . 17 𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
343319.37iv 1944 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → ∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
35 19.37v 1987 . . . . . . . . . . . . . . . . 17 (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3635biimpi 215 . . . . . . . . . . . . . . . 16 (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3734, 36syl 17 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3837eximi 1829 . . . . . . . . . . . . . 14 (∃𝑢 𝑥 = 𝑢 → ∃𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3913, 38ax-mp 5 . . . . . . . . . . . . 13 𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
403919.37iv 1944 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4140eximi 1829 . . . . . . . . . . 11 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
42 19.9v 1979 . . . . . . . . . . . 12 (∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4342biimpi 215 . . . . . . . . . . 11 (∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4441, 43syl 17 . . . . . . . . . 10 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4544eximi 1829 . . . . . . . . 9 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
46 19.9v 1979 . . . . . . . . . 10 (∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4746biimpi 215 . . . . . . . . 9 (∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4845, 47syl 17 . . . . . . . 8 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4948ss2abi 4059 . . . . . . 7 {𝑧 ∣ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩} ⊆ {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
509, 49eqsstrri 4012 . . . . . 6 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
51 vex 3465 . . . . . . . . . . 11 𝑢 ∈ V
52 vex 3465 . . . . . . . . . . 11 𝑣 ∈ V
5351, 52pm3.2i 469 . . . . . . . . . 10 (𝑢 ∈ V ∧ 𝑣 ∈ V)
5453biantru 528 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ ↔ (𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5554exbii 1842 . . . . . . . 8 (∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5655exbii 1842 . . . . . . 7 (∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5756abbii 2795 . . . . . 6 {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩} = {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
5850, 57sseqtri 4013 . . . . 5 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
59 df-opab 5212 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
60 df-opab 5212 . . . . 5 {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
6158, 59, 603sstr4i 4020 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
62 df-xp 5684 . . . . 5 (V × V) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
6362eqcomi 2734 . . . 4 {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = (V × V)
6461, 63sseqtri 4013 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ (V × V)
655, 64sstri 3986 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V)
66 df-rel 5685 . . 3 (Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V))
6766biimpri 227 . 2 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V) → Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑})
6865, 67e0a 44353 1 Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394   = wceq 1533  wex 1773  wcel 2098  {cab 2702  Vcvv 3461  wss 3944  cop 4636  {copab 5211   × cxp 5676  Rel wrel 5683
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2696
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2703  df-cleq 2717  df-clel 2802  df-rab 3419  df-v 3463  df-dif 3947  df-un 3949  df-ss 3961  df-nul 4323  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5212  df-xp 5684  df-rel 5685  df-vd1 44151  df-vd2 44159
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator