Theorem opex 4711

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 4210	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4689	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4577	. . 3 |- (/) e. _V
4	2, 3	ifex 4008	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2551	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 369   e. wcel 1767   _Vcvv 3113   (/)c0 3785   ifcif 3939   {csn 4027   {cpr 4029   <.cop 4033

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pr 4686

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-v 3115  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034

This theorem is referenced by:  otex  4712  otth2  4728  otthg  4730  oteqex2  4739  oteqex  4740  euop2  4747  opabid  4754  elopab  4755  opabn0  4778  opeliunxp  5051  elvvv  5059  opbrop  5079  relsnop  5107  xpiindi  5138  raliunxp  5142  intirr  5385  xpnz  5426  dmsnn0  5473  dmsnopg  5479  cnvcnvsn  5485  op2ndb  5492  opswap  5495  cnviin  5544  funopg  5620  dffv2  5940  fsn  6059  f1o2sn  6064  fmptsng  6082  fmptsnd  6083  fvsn  6094  resfunexg  6126  idref  6141  fveqf1o  6193  fliftel  6195  fliftel1  6196  oprabid  6308  dfoprab2  6327  oprabv  6329  rnoprab  6369  eloprabga  6373  ot1stg  6798  ot2ndg  6799  ot3rdg  6800  fo1st  6804  fo2nd  6805  opiota  6843  eloprabi  6846  mpt2sn  6874  fpar  6887  algrflem  6892  frxp  6893  xporderlem  6894  fnwelem  6898  mpt2xopoveq  6947  brtpos  6964  dmtpos  6967  rntpos  6968  tpostpos  6975  tfrlem11  7057  seqomlem1  7115  seqomlem3  7117  seqomlem4  7118  omeu  7234  iiner  7383  xpsnen  7601  xpcomco  7607  xpassen  7611  xpmapenlem  7684  unxpdomlem1  7724  fseqenlem2  8406  cda1dif  8556  fpwwe  9024  addpipq2  9314  addpqnq  9316  mulpipq2  9317  mulpqnq  9319  ordpipq  9320  prlem934  9411  addcnsr  9512  mulcnsr  9513  ltresr  9517  addcnsrec  9520  mulcnsrec  9521  axcnre  9541  om2uzrdg  12035  uzrdg0i  12038  uzrdgsuci  12039  hashfun  12461  wrdexb  12524  s1len  12580  s111  12586  wrdlen2i  12847  fsumcnv  13551  ruclem1  13825  ruclem4  13828  eucalgval2  14069  crt  14167  phimullem  14168  setsval  14514  setsres  14518  setscom  14520  strfv  14524  setsid  14531  imasaddfnlem  14783  imasaddvallem  14784  imasvscafn  14792  idfuval  15103  cofuval  15109  resfval  15119  resfval2  15120  elhoma  15217  xpcco  15310  xpcid  15316  1stfval  15318  2ndfval  15321  prfval  15326  prf1  15327  prf2  15329  evlfval  15344  curfval  15350  curf1  15352  curfcl  15359  hofval  15379  mnd1  15780  mnd1id  15781  intopsn  15782  grpss  15881  grp1  15952  symg2bas  16228  efgmval  16536  efgi  16543  efgi2  16549  frgpnabllem1  16680  frgpnabllem2  16681  rng1  17049  opsrtoslem2  17948  mat1dimelbas  18768  mat1dimbas  18769  mat1dimscm  18772  mat1dimmul  18773  mat1f1o  18775  mat1rhmelval  18777  mvmulfval  18839  m2detleib  18928  txcnp  19884  upxp  19887  uptx  19889  txdis1cn  19899  hauseqlcld  19910  txlm  19912  xkoinjcn  19951  txflf  20270  divstgplem  20382  ucnima  20547  ucnprima  20548  fmucndlem  20557  imasdsf1olem  20639  cnheiborlem  21217  ovollb2lem  21662  ovolctb  21664  ovolshftlem1  21683  ovolscalem1  21687  ovolicc1  21690  ioombl1lem3  21733  ioombl1lem4  21734  ioorval  21746  dyadval  21764  mbfimaopnlem  21825  limccnp2  22059  brbtwn  23906  brcgr  23907  eengbas  23988  ebtwntg  23989  ecgrtg  23990  elntg  23991  edgopval  24044  nbgraop  24127  nbgraopALT  24128  2trllemA  24256  constr1trl  24294  1pthonlem1  24295  1pthonlem2  24296  1pthon  24297  2pthon  24308  2pthon3v  24310  constr3lem2  24350  wlkiswwlksur  24423  wwlknext  24428  el2wlkonotot0  24576  numclwlk1lem2fv  24798  ex-br  24857  grposn  24921  gidsn  25054  ginvsn  25055  rngosn  25110  rngosn3  25132  zrdivrng  25138  cnnvg  25287  cnnvs  25290  cnnvnm  25291  h2hva  25595  h2hsm  25596  h2hnm  25597  hhssva  25879  hhsssm  25880  hhssnm  25881  hhshsslem1  25887  br8d  27164  xppreima2  27188  ofpreima  27207  cnvoprab  27246  fvproj  27526  fimaproj  27527  txomap  27528  qtophaus  27665  erdszelem9  28311  erdszelem10  28312  txpcon  28345  txsconlem  28353  ghomsn  28531  brtpid1  28601  brtpid2  28602  brtpid3  28603  fprodcnv  28718  brtp  28783  dfpo2  28789  br8  28790  br6  28791  br4  28792  br1steq  28809  br2ndeq  28810  dfdm5  28811  dfrn5  28812  elima4  28814  wfrlem14  28961  brv  29132  brtxp  29135  brpprod  29140  brpprod3b  29142  brsset  29144  brtxpsd  29149  dffun10  29169  elfuns  29170  brcart  29187  brimg  29192  brapply  29193  brcup  29194  brcap  29195  brsuccf  29196  brrestrict  29204  dfrdg4  29205  tfrqfree  29206  fvtransport  29287  brcolinear2  29313  colineardim1  29316  brsegle  29363  fvline  29399  ellines  29407  mblfinlem2  29657  filnetlem3  29829  heiborlem6  29943  heiborlem7  29944  heiborlem8  29945  gordopval  31885  gsizopval  31886  usgfis  31941  opeliun2xp  32018  lmod1lem2  32188  lmod1lem3  32189  lmod1zr  32193  zlmodzxznm  32197  zlmodzxzldeplem  32198  bnj97  33021  bnj553  33053  bnj966  33099  bnj1442  33202  bj-inftyexpiinv  33701  bj-inftyexpidisj  33703  bj-elccinfty  33707  bj-minftyccb  33718  dvhvaddval  35905  dvhvscaval  35914  dibglbN  35981  dihglbcpreN  36115  dihmeetlem4preN  36121  dihmeetlem13N  36134  hdmapfval  36645