Theorem opex 4544

Description: An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)

Assertion

Ref	Expression
opex	|- <. A , B >. e. _V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		dfopif 4044	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4522	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4410	. . 3 |- (/) e. _V
4	2, 3	ifex 3846	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2503	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 369   e. wcel 1755   _Vcvv 2962   (/)c0 3625   ifcif 3779   {csn 3865   {cpr 3867   <.cop 3871

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pr 4519

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-v 2964  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-nul 3626  df-if 3780  df-sn 3866  df-pr 3868  df-op 3872

This theorem is referenced by:  otex  4545  otth2  4561  oteqex2  4571  oteqex  4572  euop2  4579  opabid  4584  elopab  4585  opabn0  4608  opeliunxp  4877  elvvv  4885  opbrop  4903  relsnop  4931  xpiindi  4962  raliunxp  4966  intirr  5204  xpnz  5245  dmsnn0  5292  dmsnopg  5298  cnvcnvsn  5304  op2ndb  5311  opswap  5314  cnviin  5362  funopg  5438  dffv2  5752  fsn  5868  fmptsng  5887  fvsn  5898  resfunexg  5930  idref  5945  fveqf1o  5987  fliftel  5989  fliftel1  5990  oprabid  6104  dfoprab2  6122  rnoprab  6162  eloprabga  6166  ot1stg  6580  ot2ndg  6581  ot3rdg  6582  fo1st  6585  fo2nd  6586  opiota  6622  eloprabi  6625  fpar  6665  algrflem  6670  frxp  6671  xporderlem  6672  fnwelem  6676  mpt2xopoveq  6725  brtpos  6743  dmtpos  6746  rntpos  6747  tpostpos  6754  tfrlem11  6833  seqomlem1  6891  seqomlem3  6893  seqomlem4  6894  omeu  7012  iiner  7160  th3qlem2  7195  xpsnen  7383  xpcomco  7389  xpassen  7393  xpmapenlem  7466  unxpdomlem1  7505  fseqenlem2  8183  cda1dif  8333  fpwwe  8800  addpipq2  9092  addpqnq  9094  mulpipq2  9095  mulpqnq  9097  ordpipq  9098  prlem934  9189  addsrpr  9229  mulsrpr  9230  addcnsr  9289  mulcnsr  9290  ltresr  9294  addcnsrec  9297  mulcnsrec  9298  axcnre  9318  om2uzrdg  11762  uzrdg0i  11765  uzrdgsuci  11766  hashfun  12182  wrdexb  12228  s1len  12279  s111  12285  wrdlen2i  12529  fsumcnv  13223  ruclem1  13495  ruclem4  13498  eucalgval2  13738  crt  13835  phimullem  13836  setsval  14180  setsres  14184  setscom  14186  strfv  14190  setsid  14197  imasaddfnlem  14448  imasaddvallem  14449  imasvscafn  14457  idfuval  14768  cofuval  14774  resfval  14784  resfval2  14785  elhoma  14882  xpcco  14975  xpcid  14981  1stfval  14983  2ndfval  14986  prfval  14991  prf1  14992  prf2  14994  evlfval  15009  curfval  15015  curf1  15017  curfcl  15024  hofval  15044  grpss  15538  symg2bas  15882  efgmval  16188  efgi  16195  efgi2  16201  frgpnabllem1  16330  frgpnabllem2  16331  opsrtoslem2  17497  mvmulfval  18194  m2detleib  18278  txcnp  19034  upxp  19037  uptx  19039  txdis1cn  19049  hauseqlcld  19060  txlm  19062  xkoinjcn  19101  txflf  19420  divstgplem  19532  ucnima  19697  ucnprima  19698  fmucndlem  19707  imasdsf1olem  19789  cnheiborlem  20367  ovollb2lem  20812  ovolctb  20814  ovolshftlem1  20833  ovolscalem1  20837  ovolicc1  20840  ioombl1lem3  20882  ioombl1lem4  20883  ioorval  20895  dyadval  20913  mbfimaopnlem  20974  limccnp2  21208  brbtwn  22967  brcgr  22968  eengbas  23049  ebtwntg  23050  ecgrtg  23051  elntg  23052  nbgraop  23157  2trllemA  23271  constr1trl  23309  1pthonlem1  23310  1pthonlem2  23311  1pthon  23312  2pthon  23323  2pthon3v  23325  constr3lem2  23354  ex-br  23460  grposn  23524  gidsn  23657  ginvsn  23658  rngosn  23713  rngosn3  23735  zrdivrng  23741  cnnvg  23890  cnnvs  23893  cnnvnm  23894  h2hva  24198  h2hsm  24199  h2hnm  24200  hhssva  24482  hhsssm  24483  hhssnm  24484  hhshsslem1  24490  br8d  25765  xppreima2  25788  ofpreima  25807  cnvoprab  25846  erdszelem9  26934  erdszelem10  26935  txpcon  26968  txsconlem  26976  ghomsn  27153  brtpid1  27223  brtpid2  27224  brtpid3  27225  fprodcnv  27340  brtp  27405  dfpo2  27411  br8  27412  br6  27413  br4  27414  br1steq  27431  br2ndeq  27432  dfdm5  27433  dfrn5  27434  elima4  27436  wfrlem14  27583  brv  27754  brtxp  27757  brpprod  27762  brpprod3b  27764  brsset  27766  brtxpsd  27771  dffun10  27791  elfuns  27792  brcart  27809  brimg  27814  brapply  27815  brcup  27816  brcap  27817  brsuccf  27818  brrestrict  27826  dfrdg4  27827  tfrqfree  27828  fvtransport  27909  brcolinear2  27935  colineardim1  27938  brsegle  27985  fvline  28021  ellines  28029  mblfinlem2  28270  filnetlem3  28442  heiborlem6  28556  heiborlem7  28557  heiborlem8  28558  otthg  29973  oprabv  30000  wlkiswwlksur  30194  wwlknext  30199  el2wlkonotot0  30234  numclwlk1lem2fv  30529  opeliun2xp  30562  fmptsnd  30564  mpt2sn  30565  mnd1  30727  grp1  30728  rng1  30731  lmod1lem2  30736  lmod1lem3  30737  lmod1zr  30741  zlmodzxznm  30745  zlmodzxzldeplem  30746  bnj97  31558  bnj553  31590  bnj966  31636  bnj1442  31739  bj-inftyexpiinv  32108  bj-inftyexpidisj  32110  bj-elccinfty  32114  bj-minftyccb  32125  dvhvaddval  34305  dvhvscaval  34314  dibglbN  34381  dihglbcpreN  34515  dihmeetlem4preN  34521  dihmeetlem13N  34534  hdmapfval  35045