Theorem opex 4664

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 4155	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4642	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4528	. . 3 |- (/) e. _V
4	2, 3	ifex 3940	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2545	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 376   e. wcel 1904   _Vcvv 3031   (/)c0 3722   ifcif 3872   {csn 3959   {cpr 3961   <.cop 3965

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-9 1913  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451  ax-sep 4518  ax-nul 4527  ax-pr 4639

This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-3an 1009  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-ne 2643  df-v 3033  df-dif 3393  df-un 3395  df-in 3397  df-ss 3404  df-nul 3723  df-if 3873  df-sn 3960  df-pr 3962  df-op 3966

This theorem is referenced by:  otex  4665  otth2  4683  otthg  4685  oteqex2  4693  oteqex  4694  euop2  4701  opabid  4708  elopab  4709  opabn0  4732  opeliunxp  4891  elvvv  4899  opbrop  4919  relsnop  4944  xpiindi  4975  raliunxp  4979  intirr  5224  xpnz  5262  dmsnn0  5308  dmsnopg  5314  cnvcnvsn  5320  op2ndb  5327  opswap  5330  cnviin  5380  funopg  5621  dffv2  5953  fsn  6077  f1o2sn  6083  fmptsng  6101  fmptsnd  6102  fvsn  6113  fpr2g  6142  resfunexg  6146  idref  6164  fveqf1o  6218  fliftel  6220  fliftel1  6221  oprabid  6335  dfoprab2  6356  oprabv  6358  rnoprab  6398  eloprabga  6402  ot1stg  6826  ot2ndg  6827  ot3rdg  6828  fo1st  6832  fo2nd  6833  opiota  6871  eloprabi  6874  mpt2sn  6906  fpar  6919  algrflem  6924  frxp  6925  xporderlem  6926  fnwelem  6930  mpt2xopoveq  6984  brtpos  7000  dmtpos  7003  rntpos  7004  tpostpos  7011  wfrlem14  7067  tfrlem11  7124  seqomlem1  7185  seqomlem3  7187  seqomlem4  7188  omeu  7304  iiner  7453  xpsnen  7674  xpcomco  7680  xpassen  7684  xpmapenlem  7757  unxpdomlem1  7794  fseqenlem2  8474  cda1dif  8624  fpwwe  9089  addpipq2  9379  addpqnq  9381  mulpipq2  9382  mulpqnq  9384  ordpipq  9385  prlem934  9476  addcnsr  9577  mulcnsr  9578  ltresr  9582  addcnsrec  9585  mulcnsrec  9586  axcnre  9606  om2uzrdg  12208  uzrdg0i  12211  uzrdgsuci  12212  hashfun  12650  wrdexb  12730  s1len  12797  s111  12806  wrdlen2i  13093  brintclab  13142  fsumcnv  13911  fprodcnv  14114  ruclem1  14360  ruclem4  14363  eucalgval2  14619  crt  14805  phimullem  14806  setsval  15224  setsres  15229  setscom  15231  strfv  15235  setsid  15242  imasaddfnlem  15512  imasaddvallem  15513  imasvscafn  15521  idfuval  15859  cofuval  15865  resfval  15875  resfval2  15876  elhoma  16005  embedsetcestrclem  16120  xpcco  16146  xpcid  16152  1stfval  16154  2ndfval  16157  prfval  16162  prf1  16163  prf2  16165  evlfval  16180  curfval  16186  curf1  16188  curfcl  16195  hofval  16215  intopsn  16576  mgm1  16578  sgrp1  16612  mnd1  16655  mnd1OLD  16656  mnd1id  16657  grpss  16765  grp1  16836  symg2bas  17117  efgmval  17440  efgi  17447  efgi2  17453  frgpnabllem1  17587  frgpnabllem2  17588  ring1  17908  opsrtoslem2  18785  mat1dimelbas  19573  mat1dimbas  19574  mat1dimscm  19577  mat1dimmul  19578  mat1f1o  19580  mat1rhmelval  19582  mvmulfval  19644  m2detleib  19733  txcnp  20712  upxp  20715  uptx  20717  txdis1cn  20727  hauseqlcld  20738  txlm  20740  xkoinjcn  20779  txflf  21099  qustgplem  21213  ucnima  21374  ucnprima  21375  fmucndlem  21384  imasdsf1olem  21466  cnheiborlem  22060  ovollb2lem  22519  ovolctb  22521  ovolshftlem1  22540  ovolscalem1  22544  ovolicc1  22547  ioombl1lem3  22592  ioombl1lem4  22593  ioorval  22605  ioorvalOLD  22610  dyadval  22629  mbfimaopnlem  22690  limccnp2  22926  brbtwn  25008  brcgr  25009  eengbas  25090  ebtwntg  25091  ecgrtg  25092  elntg  25093  edgopval  25146  nbgraop  25230  nbgraopALT  25231  2trllemA  25359  constr1trl  25397  1pthonlem1  25398  1pthonlem2  25399  1pthon  25400  2pthon  25411  2pthon3v  25413  constr3lem2  25453  wlkiswwlksur  25526  wwlknext  25531  el2wlkonotot0  25679  numclwlk1lem2fv  25900  ex-br  25960  grposn  26024  gidsn  26157  ginvsn  26158  rngosn  26213  rngosn3  26235  zrdivrng  26241  cnnvg  26390  cnnvs  26393  cnnvnm  26394  h2hva  26708  h2hsm  26709  h2hnm  26710  hhssva  26991  hhsssm  26992  hhssnm  26993  hhshsslem1  26999  br8d  28294  xppreima2  28325  aciunf1lem  28339  ofpreima  28343  cnvoprab  28383  smatrcl  28696  smatlem  28697  fvproj  28733  fimaproj  28734  txomap  28735  qtophaus  28737  bnj97  29749  bnj553  29781  bnj966  29827  bnj1442  29930  erdszelem9  29994  erdszelem10  29995  txpcon  30027  txsconlem  30035  msubval  30235  mvhval  30244  msubvrs  30270  ghomsn  30378  brtpid1  30425  brtpid2  30426  brtpid3  30427  brtp  30460  dfpo2  30466  br8  30467  br6  30468  br4  30469  br1steq  30485  br2ndeq  30486  dfdm5  30489  dfrn5  30490  elima4  30492  fv1stcnv  30493  fv2ndcnv  30494  brv  30715  brtxp  30718  brpprod  30723  brpprod3b  30725  brsset  30727  brtxpsd  30732  dffun10  30752  elfuns  30753  brcart  30770  brimg  30775  brapply  30776  brcup  30777  brcap  30778  brsuccf  30779  brrestrict  30787  dfrecs2  30788  dfrdg4  30789  fvtransport  30870  brcolinear2  30896  colineardim1  30899  brsegle  30946  fvline  30982  ellines  30990  filnetlem3  31107  bj-inftyexpiinv  31720  bj-inftyexpidisj  31722  bj-elccinfty  31726  bj-minftyccb  31737  finxpreclem2  31852  finxp0  31853  finxp1o  31854  finxpreclem3  31855  finxpreclem4  31856  finxpreclem5  31857  finxpreclem6  31858  poimirlem9  32013  poimirlem15  32019  poimirlem17  32021  poimirlem20  32024  poimirlem24  32028  poimirlem28  32032  mblfinlem2  32042  heiborlem6  32212  heiborlem7  32213  heiborlem8  32214  dvhvaddval  34729  dvhvscaval  34738  dibglbN  34805  dihglbcpreN  34939  dihmeetlem4preN  34945  dihmeetlem13N  34958  hdmapfval  35469  elcnvlem  36278  cotrintab  36292  elimaint  36311  snhesn  36453  projf1o  37545  dvnprodlem1  37918  dvnprodlem2  37919  sge0xp  38385  hoicvr  38488  hoicvrrex  38496  hoidmv1le  38534  hoi2toco  38547  ovnlecvr2  38550  ovolval5lem2  38593  snopeqop  39145  propeqop  39146  propssopi  39147  funsndifnop  39168  structgrssvtx  39279  structgrssiedg  39280  gropd  39286  vtxvalsnop  39294  iedgvalsnop  39295  isuhgrop  39317  uhgrunop  39322  upgr0eop  39359  edgaopval  39374  isusgrop  39410  ausgrusgrb  39413  usgr0eop  39485  usgrexmpledg  39498  usgrexmpl  39499  griedg0ssusgr  39501  uhgrspanop  39532  uhgrspan1  39539  upgrres1  39544  umgrres1  39545  usgrres1  39546  nbupgrres  39602  nbupgruvtxres  39644  usgrexi  39671  cusgrexi  39672  cusgrres  39674  umgr2v2eedg  39747  umgr2v2e  39748  1wlkp1lem2  39870  ntrl2v2e  40046  eupth2eucrct  40129  eupthvdres  40147  konigsbergumgr  40164  konigsbergupgrOLD  40165  gordopval  40210  gsizopval  40211  usgfis  40266  opeliun2xp  40622  lmod1lem2  40789  lmod1lem3  40790  lmod1zr  40794  zlmodzxznm  40798  zlmodzxzldeplem  40799