Theorem opex 4663

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 4162	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4641	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4534	. . 3 |- (/) e. _V
4	2, 3	ifex 3948	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2524	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 371   e. wcel 1886   _Vcvv 3044   (/)c0 3730   ifcif 3880   {csn 3967   {cpr 3969   <.cop 3973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-9 1895  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430  ax-sep 4524  ax-nul 4533  ax-pr 4638

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 986  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2580  df-ne 2623  df-v 3046  df-dif 3406  df-un 3408  df-in 3410  df-ss 3417  df-nul 3731  df-if 3881  df-sn 3968  df-pr 3970  df-op 3974

This theorem is referenced by:  otex  4664  otth2  4682  otthg  4684  oteqex2  4692  oteqex  4693  euop2  4700  opabid  4707  elopab  4708  opabn0  4731  opeliunxp  4885  elvvv  4893  opbrop  4913  relsnop  4938  xpiindi  4969  raliunxp  4973  intirr  5217  xpnz  5255  dmsnn0  5300  dmsnopg  5306  cnvcnvsn  5312  op2ndb  5319  opswap  5322  cnviin  5372  funopg  5613  dffv2  5936  fsn  6059  f1o2sn  6065  fmptsng  6083  fmptsnd  6084  fvsn  6095  fpr2g  6123  resfunexg  6128  idref  6144  fveqf1o  6198  fliftel  6200  fliftel1  6201  oprabid  6315  dfoprab2  6334  oprabv  6336  rnoprab  6376  eloprabga  6380  ot1stg  6804  ot2ndg  6805  ot3rdg  6806  fo1st  6810  fo2nd  6811  opiota  6849  eloprabi  6852  mpt2sn  6884  fpar  6897  algrflem  6902  frxp  6903  xporderlem  6904  fnwelem  6908  mpt2xopoveq  6962  brtpos  6979  dmtpos  6982  rntpos  6983  tpostpos  6990  wfrlem14  7046  tfrlem11  7103  seqomlem1  7164  seqomlem3  7166  seqomlem4  7167  omeu  7283  iiner  7432  xpsnen  7653  xpcomco  7659  xpassen  7663  xpmapenlem  7736  unxpdomlem1  7773  fseqenlem2  8453  cda1dif  8603  fpwwe  9068  addpipq2  9358  addpqnq  9360  mulpipq2  9361  mulpqnq  9363  ordpipq  9364  prlem934  9455  addcnsr  9556  mulcnsr  9557  ltresr  9561  addcnsrec  9564  mulcnsrec  9565  axcnre  9585  om2uzrdg  12167  uzrdg0i  12170  uzrdgsuci  12171  hashfun  12606  wrdexb  12680  s1len  12741  s111  12747  wrdlen2i  13014  brintclab  13058  fsumcnv  13827  fprodcnv  14030  ruclem1  14276  ruclem4  14279  eucalgval2  14533  crt  14719  phimullem  14720  setsval  15139  setsres  15144  setscom  15146  strfv  15150  setsid  15157  imasaddfnlem  15427  imasaddvallem  15428  imasvscafn  15436  idfuval  15774  cofuval  15780  resfval  15790  resfval2  15791  elhoma  15920  embedsetcestrclem  16035  xpcco  16061  xpcid  16067  1stfval  16069  2ndfval  16072  prfval  16077  prf1  16078  prf2  16080  evlfval  16095  curfval  16101  curf1  16103  curfcl  16110  hofval  16130  intopsn  16491  mgm1  16493  sgrp1  16527  mnd1  16570  mnd1OLD  16571  mnd1id  16572  grpss  16680  grp1  16751  symg2bas  17032  efgmval  17355  efgi  17362  efgi2  17368  frgpnabllem1  17502  frgpnabllem2  17503  ring1  17823  opsrtoslem2  18701  mat1dimelbas  19489  mat1dimbas  19490  mat1dimscm  19493  mat1dimmul  19494  mat1f1o  19496  mat1rhmelval  19498  mvmulfval  19560  m2detleib  19649  txcnp  20628  upxp  20631  uptx  20633  txdis1cn  20643  hauseqlcld  20654  txlm  20656  xkoinjcn  20695  txflf  21014  qustgplem  21128  ucnima  21289  ucnprima  21290  fmucndlem  21299  imasdsf1olem  21381  cnheiborlem  21975  ovollb2lem  22434  ovolctb  22436  ovolshftlem1  22455  ovolscalem1  22459  ovolicc1  22462  ioombl1lem3  22506  ioombl1lem4  22507  ioorval  22519  ioorvalOLD  22524  dyadval  22543  mbfimaopnlem  22604  limccnp2  22840  brbtwn  24922  brcgr  24923  eengbas  25004  ebtwntg  25005  ecgrtg  25006  elntg  25007  edgopval  25060  nbgraop  25144  nbgraopALT  25145  2trllemA  25273  constr1trl  25311  1pthonlem1  25312  1pthonlem2  25313  1pthon  25314  2pthon  25325  2pthon3v  25327  constr3lem2  25367  wlkiswwlksur  25440  wwlknext  25445  el2wlkonotot0  25593  numclwlk1lem2fv  25814  ex-br  25874  grposn  25936  gidsn  26069  ginvsn  26070  rngosn  26125  rngosn3  26147  zrdivrng  26153  cnnvg  26302  cnnvs  26305  cnnvnm  26306  h2hva  26620  h2hsm  26621  h2hnm  26622  hhssva  26903  hhsssm  26904  hhssnm  26905  hhshsslem1  26911  br8d  28211  xppreima2  28242  aciunf1lem  28257  ofpreima  28261  cnvoprab  28301  smatrcl  28615  smatlem  28616  fvproj  28652  fimaproj  28653  txomap  28654  qtophaus  28656  bnj97  29670  bnj553  29702  bnj966  29748  bnj1442  29851  erdszelem9  29915  erdszelem10  29916  txpcon  29948  txsconlem  29956  msubval  30156  mvhval  30165  msubvrs  30191  ghomsn  30299  brtpid1  30346  brtpid2  30347  brtpid3  30348  brtp  30382  dfpo2  30388  br8  30389  br6  30390  br4  30391  br1steq  30407  br2ndeq  30408  dfdm5  30411  dfrn5  30412  elima4  30414  fv1stcnv  30415  fv2ndcnv  30416  brv  30637  brtxp  30640  brpprod  30645  brpprod3b  30647  brsset  30649  brtxpsd  30654  dffun10  30674  elfuns  30675  brcart  30692  brimg  30697  brapply  30698  brcup  30699  brcap  30700  brsuccf  30701  brrestrict  30709  dfrecs2  30710  dfrdg4  30711  fvtransport  30792  brcolinear2  30818  colineardim1  30821  brsegle  30868  fvline  30904  ellines  30912  filnetlem3  31029  bj-inftyexpiinv  31643  bj-inftyexpidisj  31645  bj-elccinfty  31649  bj-minftyccb  31660  finxpreclem2  31775  finxp0  31776  finxp1o  31777  finxpreclem3  31778  finxpreclem4  31779  finxpreclem5  31780  finxpreclem6  31781  poimirlem9  31942  poimirlem15  31948  poimirlem17  31950  poimirlem20  31953  poimirlem24  31957  poimirlem28  31961  mblfinlem2  31971  heiborlem6  32141  heiborlem7  32142  heiborlem8  32143  dvhvaddval  34652  dvhvscaval  34661  dibglbN  34728  dihglbcpreN  34862  dihmeetlem4preN  34868  dihmeetlem13N  34881  hdmapfval  35392  elcnvlem  36201  cotrintab  36215  elimaint  36234  snhesn  36376  projf1o  37468  dvnprodlem1  37815  dvnprodlem2  37816  sge0xp  38265  hoicvr  38364  hoicvrrex  38372  hoidmv1le  38410  hoi2toco  38423  ovnlecvr2  38426  snopeqop  38992  propeqop  38993  propssopi  38994  funsndifnop  39016  structgrssvtx  39112  structgrssiedg  39113  gropd  39119  vtxvalsnop  39127  iedgvalsnop  39128  isuhgrop  39149  uhgrunop  39154  upgr0eop  39188  upgr1eop  39189  edgaopval  39199  isusgrop  39235  ausgrusgrb  39238  usgr0eop  39307  uspgr1eop  39308  usgr1eop  39310  usgrexmpledg  39317  usgrexmpl  39318  griedg0ssusgr  39320  uhgrspanop  39351  uhgrspan1  39358  upgrres1  39363  umgrres1  39364  usgrres1  39365  nbupgrres  39421  nbupgruvtxres  39463  uvtxupgrres  39464  usgrexi  39489  cusgrexi  39490  cusgrres  39492  umgr2v2eedg  39544  umgr2v2e  39545  gordopval  39689  gsizopval  39690  usgfis  39745  opeliun2xp  40101  lmod1lem2  40268  lmod1lem3  40269  lmod1zr  40273  zlmodzxznm  40277  zlmodzxzldeplem  40278