Theorem opex 5424

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	⊢ ⟨𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		dfopif 4834	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5392	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5262	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4539	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2824	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2109  Vcvv 3447  ∅c0 4296  ifcif 4488  {csn 4589  {cpr 4591  ⟨cop 4595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596

This theorem is referenced by:  otex  5425  brv  5432  otth2  5443  otthg  5445  sbcop1  5448  oteqex2  5459  oteqex  5460  snopeqop  5466  propeqop  5467  propssopi  5468  euop2  5472  brsnop  5482  brtp  5483  opabidw  5484  opabid  5485  elopab  5487  rexopabb  5488  opabn0  5513  opeliunxp  5705  opeliun2xp  5706  elvvv  5714  opbrop  5736  relsnopg  5766  xpiindi  5799  raliunxp  5803  idrefALT  6084  intirr  6091  xpnz  6132  dmsnn0  6180  dmsnopg  6186  cnvcnvsn  6192  op2ndb  6200  opswap  6202  cnviin  6259  reuop  6266  dfpo2  6269  funopg  6550  dffv2  6956  fsn  7107  f1o2sn  7114  idref  7118  funsndifnop  7123  fmptsng  7142  fmptsnd  7143  fvsng  7154  resfunexg  7189  fveqf1o  7277  fliftel  7284  fliftel1  7285  oprabidw  7418  oprabid  7419  dfoprab2  7447  oprabv  7449  rnoprab  7494  eloprabga  7498  ot1stg  7982  ot2ndg  7983  ot3rdg  7984  fo1st  7988  fo2nd  7989  br1steqg  7990  br2ndeqg  7991  opiota  8038  eloprabi  8042  mposn  8082  fpar  8095  fsplitfpar  8097  opco1  8102  opco2  8103  frxp  8105  xporderlem  8106  fnwelem  8110  fvproj  8113  fimaproj  8114  xpord2lem  8121  xpord2pred  8124  xpord2indlem  8126  frxp3  8130  mpoxopoveq  8198  brtpos  8214  dmtpos  8217  rntpos  8218  tpostpos  8225  tfrlem11  8356  seqomlem1  8418  seqomlem3  8420  seqomlem4  8421  omeu  8549  naddcllem  8640  iiner  8762  xpsnen  9025  xpcomco  9031  xpassen  9035  xpmapenlem  9108  dif1en  9124  dif1enOLD  9126  unxpdomlem1  9197  inlresf  9867  inrresf  9869  djur  9872  djuss  9873  djuun  9879  1stinl  9880  2ndinl  9881  1stinr  9882  2ndinr  9883  fseqenlem2  9978  dju1dif  10126  fpwwe  10599  addpipq2  10889  addpqnq  10891  mulpipq2  10892  mulpqnq  10894  ordpipq  10895  prlem934  10986  addcnsr  11088  mulcnsr  11089  ltresr  11093  addcnsrec  11096  mulcnsrec  11097  axcnre  11117  om2uzrdg  13921  uzrdg0i  13924  uzrdgsuci  13925  hashfun  14402  wrdexb  14490  s1len  14571  s1nz  14572  s111  14580  wrdlen2i  14908  brintclab  14967  fsumcnv  15739  fprodcnv  15949  ruclem1  16199  ruclem4  16202  eucalgval2  16551  crth  16748  phimullem  16749  setsval  17137  setsdm  17140  setsfun  17141  setsfun0  17142  setsexstruct2  17145  setsres  17148  setscom  17150  strfv  17173  setsid  17177  imasaddfnlem  17491  imasaddvallem  17492  imasvscafn  17500  idfuval  17838  cofuval  17844  resfval  17854  resfval2  17855  elhoma  17994  embedsetcestrclem  18118  xpcco  18144  xpcid  18150  1stfval  18152  2ndfval  18155  prfval  18160  prf1  18161  prf2  18163  evlfval  18178  curfval  18184  curf1  18186  curfcl  18193  hofval  18213  intopsn  18581  mgm1  18585  sgrp1  18656  mnd1  18706  mnd1id  18707  grpss  18886  grp1  18979  symg2bas  19323  efgmval  19642  efgi  19649  efgi2  19655  frgpnabllem1  19803  frgpnabllem2  19804  ring1  20219  rngqiprngimfv  21208  rngqiprngimf1  21210  opsrtoslem2  21963  mat1dimelbas  22358  mat1dimbas  22359  mat1dimscm  22362  mat1dimmul  22363  mat1f1o  22365  mat1rhmelval  22367  mvmulfval  22429  m2detleib  22518  txcnp  23507  upxp  23510  uptx  23512  txdis1cn  23522  hauseqlcld  23533  txlm  23535  xkoinjcn  23574  txflf  23893  qustgplem  24008  ucnima  24168  ucnprima  24169  fmucndlem  24178  imasdsf1olem  24261  cnheiborlem  24853  ovollb2lem  25389  ovolctb  25391  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  ioombl1lem3  25461  ioombl1lem4  25462  ioorval  25475  dyadval  25493  mbfimaopnlem  25556  limccnp2  25793  addsval  27869  mulsval  28012  precsexlem1  28109  precsexlem2  28110  precsexlem3  28111  om2noseqrdg  28198  noseqrdg0  28201  noseqrdgsuc  28202  brbtwn  28826  brcgr  28827  eengbas  28908  ebtwntg  28909  ecgrtg  28910  elntg  28911  structvtxval  28948  structgrssvtx  28951  structgrssiedg  28952  gropd  28958  isuhgrop  28997  uhgrunop  29002  upgrop  29021  upgr0eop  29041  upgrunop  29046  umgrunop  29048  isuspgrop  29088  isusgrop  29089  ausgrusgrb  29092  usgr0eop  29173  griedg0ssusgr  29192  uhgrspanop  29223  uhgrspan1  29230  upgrres  29233  umgrres  29234  usgrres  29235  upgrres1  29240  umgrres1  29241  usgrres1  29242  usgrexi  29368  cusgrexi  29370  cffldtocusgr  29374  cffldtocusgrOLD  29375  cusgrres  29376  vtxdgop  29398  umgr2v2e  29453  wlkp1lem2  29602  wlkswwlksf1o  29809  wwlksnext  29823  eupth2eucrct  30146  eupthvdres  30164  konigsbergumgr  30180  numclwwlk1lem2fv  30285  numclwlk1lem1  30298  ex-br  30360  ex-fpar  30391  cnnvg  30607  cnnvs  30609  cnnvnm  30610  h2hva  30903  h2hsm  30904  h2hnm  30905  hhssva  31186  hhsssm  31187  hhssnm  31188  hhshsslem1  31196  br8d  32538  xppreima2  32575  aciunf1lem  32586  ofpreima  32589  rlocaddval  33219  rlocmulval  33220  linds2eq  33352  smatrcl  33786  smatlem  33787  txomap  33824  qtophaus  33826  hgt750lemb  34647  bnj97  34856  bnj553  34888  bnj966  34934  bnj1442  35039  erdszelem9  35186  erdszelem10  35187  txpconn  35219  txsconnlem  35227  goel  35334  goeleq12bg  35336  gonafv  35337  gonanegoal  35339  sat1el2xp  35366  fmlaomn0  35377  gonan0  35379  goaln0  35380  gonarlem  35381  gonar  35382  goalrlem  35383  goalr  35384  fmla0disjsuc  35385  fmlasucdisj  35386  satffunlem  35388  satffunlem1lem1  35389  satffunlem2lem1  35391  satfv0fvfmla0  35400  sategoelfvb  35406  prv1n  35418  msubval  35512  mvhval  35521  msubvrs  35547  brtpid1  35708  brtpid2  35709  brtpid3  35710  br8  35743  br6  35744  br4  35745  dfdm5  35760  dfrn5  35761  elima4  35763  fv1stcnv  35764  fv2ndcnv  35765  brtxp  35868  brpprod  35873  brpprod3b  35875  brsset  35877  brtxpsd  35882  dffun10  35902  elfuns  35903  brcart  35920  brimg  35925  brapply  35926  brcup  35927  brcap  35928  brsuccf  35929  brrestrict  35937  dfrecs2  35938  dfrdg4  35939  fvtransport  36020  brcolinear2  36046  colineardim1  36049  brsegle  36096  fvline  36132  ellines  36140  filnetlem3  36368  bj-inftyexpitaufo  37190  bj-inftyexpitaudisj  37193  bj-inftyexpiinv  37196  bj-inftyexpidisj  37198  bj-elccinfty  37202  bj-minftyccb  37213  finxpreclem2  37378  finxp0  37379  finxp1o  37380  finxpreclem3  37381  finxpreclem4  37382  finxpreclem5  37383  finxpreclem6  37384  poimirlem9  37623  poimirlem15  37629  poimirlem17  37631  poimirlem20  37634  poimirlem24  37638  poimirlem28  37642  mblfinlem2  37652  heiborlem6  37810  heiborlem7  37811  heiborlem8  37812  grposnOLD  37876  rngosn3  37918  gidsn  37946  zrdivrng  37947  brxrn  38356  br1cossxrnres  38439  dvhvaddval  41084  dvhvscaval  41093  dibglbN  41160  dihglbcpreN  41294  dihmeetlem4preN  41300  dihmeetlem13N  41313  hdmapfval  41821  elcnvlem  43590  cotrintab  43603  elimaint  43638  snhesn  43775  nregmodellem  45006  projf1o  45191  dvnprodlem1  45944  dvnprodlem2  45945  sge0xp  46427  hoicvr  46546  hoicvrrex  46554  hoidmv1le  46592  hoi2toco  46605  ovnlecvr2  46608  ovolval5lem2  46651  fsetsnf1  47053  setsidel  47377  prproropf1olem3  47506  prproropf1olem4  47507  prproropreud  47510  isisubgr  47862  ushggricedg  47927  gpgusgralem  48047  gpgvtxedg0  48054  gpgvtxedg1  48055  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  gpg3nbgrvtx0  48067  gpg3nbgrvtx0ALT  48068  gpg3nbgrvtx1  48069  gpg5nbgrvtx03star  48071  gpg5nbgr3star  48072  gpg3kgrtriex  48080  gpgprismgr4cycllem2  48086  gpgprismgr4cycllem6  48090  gpgprismgr4cycllem7  48091  gpgprismgr4cycllem10  48094  lmod1lem2  48477  lmod1lem3  48478  lmod1zr  48482  zlmodzxznm  48486  zlmodzxzldeplem  48487  rrx2xpref1o  48707  line2x  48743  inlinecirc02plem  48775  iinxp  48819  ovsng  48846  eloprab1st2nd  48856  tposid  48873  tposidres  48874  initc  49080  rescofuf  49082  idfurcl  49087  imaf1hom  49097  oppffn  49113  oppfvalg  49115  swapfval  49251  swapf1a  49258  swapf2a  49260  swapf1  49261  swapf2  49263  fucofvalg  49307  fucofval  49308  fucofvalne  49314  fuco21  49325  fucof21  49336  prcofvalg  49365  prcofvala  49366  prcofval  49367  thincciso  49442  setc1ocofval  49483  functermceu  49499  termcfuncval  49521  fucterm  49531  0fucterm  49532  relran  49613  ranval3  49620  ranrcl4lem  49627  ranup  49631  initocmd  49658