NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  opeq Unicode version

Theorem opeq 4619
Description: Any class is equal to an ordered pair. (Contributed by Scott Fenton, 8-Apr-2021.)
Assertion
Ref Expression
opeq Proj1 Proj2

Proof of Theorem opeq
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-op 4566 . 2 Proj1 Proj2 Proj1 Phi Proj2 Phi 0c
2 df-proj1 4567 . . . . . . 7 Proj1 Phi
32rexeqi 2812 . . . . . 6 Proj1 Phi Phi Phi
4 phieq 4570 . . . . . . . 8 Phi Phi
54eleq1d 2419 . . . . . . 7 Phi Phi
65rexab 2999 . . . . . 6 Phi Phi Phi Phi
7 ancom 437 . . . . . . . . 9 Phi Phi Phi Phi
8 eleq1 2413 . . . . . . . . . 10 Phi Phi
98pm5.32i 618 . . . . . . . . 9 Phi Phi Phi
107, 9bitr4i 243 . . . . . . . 8 Phi Phi Phi
1110exbii 1582 . . . . . . 7 Phi Phi Phi
12 19.41v 1901 . . . . . . 7 Phi Phi
13 ancom 437 . . . . . . 7 Phi Phi
1411, 12, 133bitri 262 . . . . . 6 Phi Phi Phi
153, 6, 143bitri 262 . . . . 5 Proj1 Phi Phi
1615abbii 2465 . . . 4 Proj1 Phi Phi
17 df-rab 2623 . . . 4 Phi Phi
1816, 17eqtr4i 2376 . . 3 Proj1 Phi Phi
19 df-proj2 4568 . . . . . . 7 Proj2 Phi 0c
2019rexeqi 2812 . . . . . 6 Proj2 Phi 0c Phi 0c Phi 0c
214uneq1d 3417 . . . . . . . 8 Phi 0c Phi 0c
2221eleq1d 2419 . . . . . . 7 Phi 0c Phi 0c
2322rexab 2999 . . . . . 6 Phi 0c Phi 0c Phi 0c Phi 0c
24 ancom 437 . . . . . . . . 9 Phi 0c Phi 0c Phi 0c Phi 0c
25 eleq1 2413 . . . . . . . . . 10 Phi 0c Phi 0c
2625pm5.32i 618 . . . . . . . . 9 Phi 0c Phi 0c Phi 0c
2724, 26bitr4i 243 . . . . . . . 8 Phi 0c Phi 0c Phi 0c
2827exbii 1582 . . . . . . 7 Phi 0c Phi 0c Phi 0c
29 19.41v 1901 . . . . . . 7 Phi 0c Phi 0c
30 ancom 437 . . . . . . 7 Phi 0c Phi 0c
3128, 29, 303bitri 262 . . . . . 6 Phi 0c Phi 0c Phi 0c
3220, 23, 313bitri 262 . . . . 5 Proj2 Phi 0c Phi 0c
3332abbii 2465 . . . 4 Proj2 Phi 0c Phi 0c
34 df-rab 2623 . . . 4 Phi 0c Phi 0c
3533, 34eqtr4i 2376 . . 3 Proj2 Phi 0c Phi 0c
3618, 35uneq12i 3416 . 2 Proj1 Phi Proj2 Phi 0c Phi Phi 0c
37 unrab 3526 . . 3 Phi Phi 0c Phi Phi 0c
38 rabid2 2788 . . . 4 Phi Phi 0c Phi Phi 0c
39 vex 2862 . . . . . . 7
4039phiall 4618 . . . . . 6 Phi Phi 0c
41 19.43 1605 . . . . . 6 Phi Phi 0c Phi Phi 0c
4240, 41mpbi 199 . . . . 5 Phi Phi 0c
4342a1i 10 . . . 4 Phi Phi 0c
4438, 43mprgbir 2684 . . 3 Phi Phi 0c
4537, 44eqtr4i 2376 . 2 Phi Phi 0c
461, 36, 453eqtrri 2378 1 Proj1 Proj2
Colors of variables: wff setvar class
Syntax hints:   wo 357   wa 358  wex 1541   wceq 1642   wcel 1710  cab 2339  wrex 2615  crab 2618   cun 3207  csn 3737  0cc0c 4374  cop 4561   Phi cphi 4562   Proj1 cproj1 4563   Proj2 cproj2 4564
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4078  ax-xp 4079  ax-cnv 4080  ax-1c 4081  ax-sset 4082  ax-si 4083  ax-ins2 4084  ax-ins3 4085  ax-typlower 4086  ax-sn 4087
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2478  df-ne 2518  df-ral 2619  df-rex 2620  df-rab 2623  df-v 2861  df-sbc 3047  df-nin 3211  df-compl 3212  df-in 3213  df-un 3214  df-dif 3215  df-symdif 3216  df-ss 3259  df-nul 3551  df-if 3663  df-pw 3724  df-sn 3741  df-pr 3742  df-uni 3892  df-int 3927  df-opk 4058  df-1c 4136  df-pw1 4137  df-uni1 4138  df-xpk 4185  df-cnvk 4186  df-ins2k 4187  df-ins3k 4188  df-imak 4189  df-cok 4190  df-p6 4191  df-sik 4192  df-ssetk 4193  df-imagek 4194  df-idk 4195  df-0c 4377  df-addc 4378  df-nnc 4379  df-phi 4565  df-op 4566  df-proj1 4567  df-proj2 4568
This theorem is referenced by:  opeqexb  4620  xpvv  4843  ssrel  4844  proj1eldm  4927  co01  5093  1stfo  5505  2ndfo  5506  swapf1o  5511  otsnelsi3  5805  xpassenlem  6056  xpassen  6057  nncdiv3lem1  6275  dmfrec  6316  fnfreclem2  6318
  Copyright terms: Public domain W3C validator