Theorem opex 4678

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 4178	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4656	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4549	. . 3 |- (/) e. _V
4	2, 3	ifex 3974	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2504	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 370   e. wcel 1867   _Vcvv 3078   (/)c0 3758   ifcif 3906   {csn 3993   {cpr 3995   <.cop 3999

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-9 1871  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398  ax-sep 4540  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-ne 2618  df-v 3080  df-dif 3436  df-un 3438  df-in 3440  df-ss 3447  df-nul 3759  df-if 3907  df-sn 3994  df-pr 3996  df-op 4000

This theorem is referenced by:  otex  4679  otth2  4695  otthg  4697  oteqex2  4705  oteqex  4706  euop2  4713  opabid  4720  elopab  4721  opabn0  4744  opeliunxp  4898  elvvv  4906  opbrop  4926  relsnop  4951  xpiindi  4982  raliunxp  4986  intirr  5230  xpnz  5268  dmsnn0  5313  dmsnopg  5319  cnvcnvsn  5325  op2ndb  5332  opswap  5335  cnviin  5385  funopg  5625  dffv2  5946  fsn  6068  f1o2sn  6074  fmptsng  6092  fmptsnd  6093  fvsn  6104  fpr2g  6132  resfunexg  6137  idref  6153  fveqf1o  6207  fliftel  6209  fliftel1  6210  oprabid  6324  dfoprab2  6343  oprabv  6345  rnoprab  6385  eloprabga  6389  ot1stg  6813  ot2ndg  6814  ot3rdg  6815  fo1st  6819  fo2nd  6820  opiota  6858  eloprabi  6861  mpt2sn  6890  fpar  6903  algrflem  6908  frxp  6909  xporderlem  6910  fnwelem  6914  mpt2xopoveq  6965  brtpos  6982  dmtpos  6985  rntpos  6986  tpostpos  6993  wfrlem14  7049  tfrlem11  7106  seqomlem1  7167  seqomlem3  7169  seqomlem4  7170  omeu  7286  iiner  7435  xpsnen  7654  xpcomco  7660  xpassen  7664  xpmapenlem  7737  unxpdomlem1  7774  fseqenlem2  8452  cda1dif  8602  fpwwe  9067  addpipq2  9357  addpqnq  9359  mulpipq2  9360  mulpqnq  9362  ordpipq  9363  prlem934  9454  addcnsr  9555  mulcnsr  9556  ltresr  9560  addcnsrec  9563  mulcnsrec  9564  axcnre  9584  om2uzrdg  12163  uzrdg0i  12166  uzrdgsuci  12167  hashfun  12600  wrdexb  12666  s1len  12727  s111  12733  wrdlen2i  13000  brintclab  13044  fsumcnv  13812  fprodcnv  14015  ruclem1  14261  ruclem4  14264  eucalgval2  14518  crt  14704  phimullem  14705  setsval  15124  setsres  15129  setscom  15131  strfv  15135  setsid  15142  imasaddfnlem  15412  imasaddvallem  15413  imasvscafn  15421  idfuval  15759  cofuval  15765  resfval  15775  resfval2  15776  elhoma  15905  embedsetcestrclem  16020  xpcco  16046  xpcid  16052  1stfval  16054  2ndfval  16057  prfval  16062  prf1  16063  prf2  16065  evlfval  16080  curfval  16086  curf1  16088  curfcl  16095  hofval  16115  intopsn  16476  mgm1  16478  sgrp1  16512  mnd1  16555  mnd1OLD  16556  mnd1id  16557  grpss  16665  grp1  16736  symg2bas  17017  efgmval  17340  efgi  17347  efgi2  17353  frgpnabllem1  17487  frgpnabllem2  17488  ring1  17808  opsrtoslem2  18686  mat1dimelbas  19473  mat1dimbas  19474  mat1dimscm  19477  mat1dimmul  19478  mat1f1o  19480  mat1rhmelval  19482  mvmulfval  19544  m2detleib  19633  txcnp  20612  upxp  20615  uptx  20617  txdis1cn  20627  hauseqlcld  20638  txlm  20640  xkoinjcn  20679  txflf  20998  qustgplem  21112  ucnima  21273  ucnprima  21274  fmucndlem  21283  imasdsf1olem  21365  cnheiborlem  21959  ovollb2lem  22418  ovolctb  22420  ovolshftlem1  22439  ovolscalem1  22443  ovolicc1  22446  ioombl1lem3  22490  ioombl1lem4  22491  ioorval  22503  ioorvalOLD  22508  dyadval  22527  mbfimaopnlem  22588  limccnp2  22824  brbtwn  24906  brcgr  24907  eengbas  24988  ebtwntg  24989  ecgrtg  24990  elntg  24991  edgopval  25044  nbgraop  25127  nbgraopALT  25128  2trllemA  25256  constr1trl  25294  1pthonlem1  25295  1pthonlem2  25296  1pthon  25297  2pthon  25308  2pthon3v  25310  constr3lem2  25350  wlkiswwlksur  25423  wwlknext  25428  el2wlkonotot0  25576  numclwlk1lem2fv  25797  ex-br  25857  grposn  25919  gidsn  26052  ginvsn  26053  rngosn  26108  rngosn3  26130  zrdivrng  26136  cnnvg  26285  cnnvs  26288  cnnvnm  26289  h2hva  26603  h2hsm  26604  h2hnm  26605  hhssva  26886  hhsssm  26887  hhssnm  26888  hhshsslem1  26894  br8d  28198  xppreima2  28230  aciunf1lem  28245  ofpreima  28249  cnvoprab  28293  smatrcl  28611  smatlem  28612  fvproj  28648  fimaproj  28649  txomap  28650  qtophaus  28652  bnj97  29666  bnj553  29698  bnj966  29744  bnj1442  29847  erdszelem9  29911  erdszelem10  29912  txpcon  29944  txsconlem  29952  msubval  30152  mvhval  30161  msubvrs  30187  ghomsn  30295  brtpid1  30342  brtpid2  30343  brtpid3  30344  brtp  30377  dfpo2  30383  br8  30384  br6  30385  br4  30386  br1steq  30402  br2ndeq  30403  dfdm5  30406  dfrn5  30407  elima4  30409  fv1stcnv  30410  fv2ndcnv  30411  brv  30630  brtxp  30633  brpprod  30638  brpprod3b  30640  brsset  30642  brtxpsd  30647  dffun10  30667  elfuns  30668  brcart  30685  brimg  30690  brapply  30691  brcup  30692  brcap  30693  brsuccf  30694  brrestrict  30702  dfrecs2  30703  dfrdg4  30704  fvtransport  30785  brcolinear2  30811  colineardim1  30814  brsegle  30861  fvline  30897  ellines  30905  filnetlem3  31022  bj-inftyexpiinv  31596  bj-inftyexpidisj  31598  bj-elccinfty  31602  bj-minftyccb  31613  poimirlem9  31857  poimirlem15  31863  poimirlem17  31865  poimirlem20  31868  poimirlem24  31872  poimirlem28  31876  mblfinlem2  31886  heiborlem6  32056  heiborlem7  32057  heiborlem8  32058  dvhvaddval  34571  dvhvscaval  34580  dibglbN  34647  dihglbcpreN  34781  dihmeetlem4preN  34787  dihmeetlem13N  34800  hdmapfval  35311  elimaint  36094  snhesn  36234  dvnprodlem1  37608  dvnprodlem2  37609  snopeqop  38611  propeqop  38612  propssopi  38613  funsndifnop  38628  vtxvalsnop  38700  iedgvalsnop  38701  uhgrop  38719  uhgrres  38723  uhgrun  38724  gordopval  38764  gsizopval  38765  usgfis  38820  opeliun2xp  39178  lmod1lem2  39345  lmod1lem3  39346  lmod1zr  39350  zlmodzxznm  39354  zlmodzxzldeplem  39355