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 44898
Description: Virtual deduction proof of relopab 5836. 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 5836 is relopabVD 44898 without virtual deductions and was automatically derived from relopabVD 44898.
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 3481 . . . . . 6 𝑥 ∈ V
2 vex 3481 . . . . . 6 𝑦 ∈ V
31, 2pm3.2i 470 . . . . 5 (𝑥 ∈ V ∧ 𝑦 ∈ V)
43a1i 11 . . . 4 (𝜑 → (𝑥 ∈ V ∧ 𝑦 ∈ V))
54ssopab2i 5559 . . 3 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)}
63biantru 529 . . . . . . . . . 10 (𝑧 = ⟨𝑥, 𝑦⟩ ↔ (𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
76exbii 1844 . . . . . . . . 9 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
87exbii 1844 . . . . . . . 8 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ ↔ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V)))
98abbii 2806 . . . . . . 7 {𝑧 ∣ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
10 ax6ev 1966 . . . . . . . . . . . . . . 15 𝑢 𝑢 = 𝑥
11 equcom 2014 . . . . . . . . . . . . . . . 16 (𝑢 = 𝑥𝑥 = 𝑢)
1211exbii 1844 . . . . . . . . . . . . . . 15 (∃𝑢 𝑢 = 𝑥 ↔ ∃𝑢 𝑥 = 𝑢)
1310, 12mpbi 230 . . . . . . . . . . . . . 14 𝑢 𝑥 = 𝑢
14 ax6ev 1966 . . . . . . . . . . . . . . . . . . 19 𝑣 𝑣 = 𝑦
15 equcom 2014 . . . . . . . . . . . . . . . . . . . 20 (𝑣 = 𝑦𝑦 = 𝑣)
1615exbii 1844 . . . . . . . . . . . . . . . . . . 19 (∃𝑣 𝑣 = 𝑦 ↔ ∃𝑣 𝑦 = 𝑣)
1714, 16mpbi 230 . . . . . . . . . . . . . . . . . 18 𝑣 𝑦 = 𝑣
18 idn1 44571 . . . . . . . . . . . . . . . . . . . . . . . 24 (   𝑦 = 𝑣   ▶   𝑦 = 𝑣   )
19 opeq2 4878 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦 = 𝑣 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩)
2018, 19e1a 44624 . . . . . . . . . . . . . . . . . . . . . . 23 (   𝑦 = 𝑣   ▶   𝑥, 𝑦⟩ = ⟨𝑥, 𝑣   )
21 idn2 44610 . . . . . . . . . . . . . . . . . . . . . . . 24 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥 = 𝑢   )
22 opeq1 4877 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥 = 𝑢 → ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩)
2321, 22e2 44628 . . . . . . . . . . . . . . . . . . . . . . 23 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥, 𝑣⟩ = ⟨𝑢, 𝑣   )
24 eqeq1 2738 . . . . . . . . . . . . . . . . . . . . . . . 24 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ ↔ ⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩))
2524biimprd 248 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑣⟩ → (⟨𝑥, 𝑣⟩ = ⟨𝑢, 𝑣⟩ → ⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩))
2620, 23, 25e12 44721 . . . . . . . . . . . . . . . . . . . . . 22 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   𝑥, 𝑦⟩ = ⟨𝑢, 𝑣   )
27 eqeq2 2746 . . . . . . . . . . . . . . . . . . . . . . 23 (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑢, 𝑣⟩))
2827biimpd 229 . . . . . . . . . . . . . . . . . . . . . 22 (⟨𝑥, 𝑦⟩ = ⟨𝑢, 𝑣⟩ → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
2926, 28e2 44628 . . . . . . . . . . . . . . . . . . . . 21 (   𝑦 = 𝑣   ,   𝑥 = 𝑢   ▶   (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)   )
3029in2 44602 . . . . . . . . . . . . . . . . . . . 20 (   𝑦 = 𝑣   ▶   (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))   )
3130in1 44568 . . . . . . . . . . . . . . . . . . 19 (𝑦 = 𝑣 → (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
3231eximi 1831 . . . . . . . . . . . . . . . . . 18 (∃𝑣 𝑦 = 𝑣 → ∃𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩)))
3317, 32ax-mp 5 . . . . . . . . . . . . . . . . 17 𝑣(𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
343319.37iv 1945 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑢 → ∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩))
35 19.37v 1988 . . . . . . . . . . . . . . . . 17 (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) ↔ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3635biimpi 216 . . . . . . . . . . . . . . . 16 (∃𝑣(𝑧 = ⟨𝑥, 𝑦⟩ → 𝑧 = ⟨𝑢, 𝑣⟩) → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3734, 36syl 17 . . . . . . . . . . . . . . 15 (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3837eximi 1831 . . . . . . . . . . . . . 14 (∃𝑢 𝑥 = 𝑢 → ∃𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩))
3913, 38ax-mp 5 . . . . . . . . . . . . 13 𝑢(𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
403919.37iv 1945 . . . . . . . . . . . 12 (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4140eximi 1831 . . . . . . . . . . 11 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
42 19.9v 1980 . . . . . . . . . . . 12 (∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4342biimpi 216 . . . . . . . . . . 11 (∃𝑦𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4441, 43syl 17 . . . . . . . . . 10 (∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4544eximi 1831 . . . . . . . . 9 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
46 19.9v 1980 . . . . . . . . . 10 (∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4746biimpi 216 . . . . . . . . 9 (∃𝑥𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4845, 47syl 17 . . . . . . . 8 (∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩)
4948ss2abi 4076 . . . . . . 7 {𝑧 ∣ ∃𝑥𝑦 𝑧 = ⟨𝑥, 𝑦⟩} ⊆ {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
509, 49eqsstrri 4030 . . . . . 6 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩}
51 vex 3481 . . . . . . . . . . 11 𝑢 ∈ V
52 vex 3481 . . . . . . . . . . 11 𝑣 ∈ V
5351, 52pm3.2i 470 . . . . . . . . . 10 (𝑢 ∈ V ∧ 𝑣 ∈ V)
5453biantru 529 . . . . . . . . 9 (𝑧 = ⟨𝑢, 𝑣⟩ ↔ (𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5554exbii 1844 . . . . . . . 8 (∃𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5655exbii 1844 . . . . . . 7 (∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩ ↔ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)))
5756abbii 2806 . . . . . 6 {𝑧 ∣ ∃𝑢𝑣 𝑧 = ⟨𝑢, 𝑣⟩} = {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
5850, 57sseqtri 4031 . . . . 5 {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))} ⊆ {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
59 df-opab 5210 . . . . 5 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} = {𝑧 ∣ ∃𝑥𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ (𝑥 ∈ V ∧ 𝑦 ∈ V))}
60 df-opab 5210 . . . . 5 {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = {𝑧 ∣ ∃𝑢𝑣(𝑧 = ⟨𝑢, 𝑣⟩ ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V))}
6158, 59, 603sstr4i 4038 . . . 4 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
62 df-xp 5694 . . . . 5 (V × V) = {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)}
6362eqcomi 2743 . . . 4 {⟨𝑢, 𝑣⟩ ∣ (𝑢 ∈ V ∧ 𝑣 ∈ V)} = (V × V)
6461, 63sseqtri 4031 . . 3 {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ V ∧ 𝑦 ∈ V)} ⊆ (V × V)
655, 64sstri 4004 . 2 {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V)
66 df-rel 5695 . . 3 (Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑} ↔ {⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V))
6766biimpri 228 . 2 ({⟨𝑥, 𝑦⟩ ∣ 𝜑} ⊆ (V × V) → Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑})
6865, 67e0a 44769 1 Rel {⟨𝑥, 𝑦⟩ ∣ 𝜑}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395   = wceq 1536  wex 1775  wcel 2105  {cab 2711  Vcvv 3477  wss 3962  cop 4636  {copab 5209   × cxp 5686  Rel wrel 5693
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-opab 5210  df-xp 5694  df-rel 5695  df-vd1 44567  df-vd2 44575
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator