Theorem opex 5120

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 4590	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5097	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 4982	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4325	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2879	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 384   ∈ wcel 2156  Vcvv 3389  ∅c0 4114  ifcif 4277  {csn 4368  {cpr 4370  ⟨cop 4374

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2782  ax-sep 4973  ax-nul 4981  ax-pr 5094

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2791  df-cleq 2797  df-clel 2800  df-nfc 2935  df-v 3391  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4115  df-if 4278  df-sn 4369  df-pr 4371  df-op 4375

This theorem is referenced by:  otex  5121  brv  5128  otth2  5139  otthg  5141  oteqex2  5150  oteqex  5151  snopeqop  5158  snopeqopOLD  5159  propeqop  5160  propssopi  5161  euop2  5165  opabid  5175  elopab  5176  opabn0  5199  opeliunxp  5368  elvvv  5376  opbrop  5398  relsnopg  5424  relsnopOLD  5428  xpiindi  5457  raliunxp  5461  idrefALT  5717  intirr  5723  xpnz  5762  dmsnn0  5809  dmsnopg  5816  cnvcnvsn  5822  op2ndb  5831  opswap  5834  cnviin  5884  funopg  6133  dffv2  6490  fsn  6623  f1o2sn  6629  idref  6633  funsndifnop  6638  fmptsng  6657  fmptsnd  6658  fvsn  6669  fpr2g  6698  resfunexg  6702  fveqf1o  6779  fliftel  6781  fliftel1  6782  oprabid  6903  dfoprab2  6929  oprabv  6931  rnoprab  6971  eloprabga  6975  ot1stg  7410  ot2ndg  7411  ot3rdg  7412  fo1st  7416  fo2nd  7417  br1steqg  7418  br2ndeqg  7419  opiota  7459  eloprabi  7463  mpt2sn  7500  fpar  7513  algrflem  7518  frxp  7519  xporderlem  7520  fnwelem  7524  mpt2xopoveq  7578  brtpos  7594  dmtpos  7597  rntpos  7598  tpostpos  7605  wfrlem14  7662  tfrlem11  7718  seqomlem1  7779  seqomlem3  7781  seqomlem4  7782  omeu  7900  iiner  8052  xpsnen  8281  xpcomco  8287  xpassen  8291  xpmapenlem  8364  unxpdomlem1  8401  inlresf  9021  inrresf  9023  djur  9026  djuss  9027  djuun  9033  1stinl  9034  2ndinl  9035  1stinr  9036  2ndinr  9037  fseqenlem2  9129  cda1dif  9281  fpwwe  9751  addpipq2  10041  addpqnq  10043  mulpipq2  10044  mulpqnq  10046  ordpipq  10047  prlem934  10138  addcnsr  10239  mulcnsr  10240  ltresr  10244  addcnsrec  10247  mulcnsrec  10248  axcnre  10268  om2uzrdg  12977  uzrdg0i  12980  uzrdgsuci  12981  hashfun  13439  wrdexb  13525  s1len  13599  s1nz  13600  s111  13608  wrdlen2i  13909  brintclab  13963  fsumcnv  14725  fprodcnv  14932  ruclem1  15178  ruclem4  15181  eucalgval2  15511  crth  15698  phimullem  15699  setsval  16097  setsdm  16101  setsfun  16102  setsfun0  16103  setsexstruct2  16106  setsres  16110  setscom  16112  strfv  16116  setsid  16123  imasaddfnlem  16391  imasaddvallem  16392  imasvscafn  16400  idfuval  16738  cofuval  16744  resfval  16754  resfval2  16755  elhoma  16884  embedsetcestrclem  17000  xpcco  17026  xpcid  17032  1stfval  17034  2ndfval  17037  prfval  17042  prf1  17043  prf2  17045  evlfval  17060  curfval  17066  curf1  17068  curfcl  17075  hofval  17095  intopsn  17456  mgm1  17460  sgrp1  17496  mnd1  17534  mnd1id  17535  grpss  17643  grp1  17725  symg2bas  18017  efgmval  18324  efgi  18331  efgi2  18337  frgpnabllem1  18475  frgpnabllem2  18476  ring1  18802  opsrtoslem2  19691  mat1dimelbas  20486  mat1dimbas  20487  mat1dimscm  20490  mat1dimmul  20491  mat1f1o  20493  mat1rhmelval  20495  mvmulfval  20557  m2detleib  20646  txcnp  21635  upxp  21638  uptx  21640  txdis1cn  21650  hauseqlcld  21661  txlm  21663  xkoinjcn  21702  txflf  22021  qustgplem  22135  ucnima  22296  ucnprima  22297  fmucndlem  22306  imasdsf1olem  22389  cnheiborlem  22964  ovollb2lem  23467  ovolctb  23469  ovolshftlem1  23488  ovolscalem1  23492  ovolicc1  23495  ioombl1lem3  23539  ioombl1lem4  23540  ioorval  23553  dyadval  23571  mbfimaopnlem  23634  limccnp2  23868  brbtwn  25991  brcgr  25992  eengbas  26073  ebtwntg  26074  ecgrtg  26075  elntg  26076  structvtxval  26122  structgrssvtx  26125  structgrssiedg  26126  structgrssvtxOLD  26128  structgrssiedgOLD  26129  gropd  26135  isuhgrop  26177  uhgrunop  26182  upgrop  26201  upgr0eop  26221  upgrunop  26226  umgrunop  26228  isuspgrop  26269  isusgrop  26270  ausgrusgrb  26273  usgr0eop  26352  usgrexmpl  26369  griedg0ssusgr  26371  uhgrspanop  26402  uhgrspan1  26409  upgrres  26412  umgrres  26413  usgrres  26414  upgrres1  26419  umgrres1  26420  usgrres1  26421  usgrexi  26563  cusgrexi  26565  cffldtocusgr  26569  cusgrres  26570  vtxdgop  26592  umgr2v2e  26647  wlkp1lem2  26797  wlkswwlksf1o  27004  wlkwwlksurOLD  27023  wwlksnext  27028  eupth2eucrct  27388  eupthvdres  27406  konigsbergumgr  27422  numclwwlk1lem2fv  27533  numclwlk1lem1  27547  ex-br  27617  cnnvg  27859  cnnvs  27861  cnnvnm  27862  h2hva  28157  h2hsm  28158  h2hnm  28159  hhssva  28440  hhsssm  28441  hhssnm  28442  hhshsslem1  28450  br8d  29745  xppreima2  29775  aciunf1lem  29787  ofpreima  29790  cnvoprabOLD  29823  smatrcl  30185  smatlem  30186  fvproj  30222  fimaproj  30223  txomap  30224  qtophaus  30226  hgt750lemb  31057  bnj97  31257  bnj553  31289  bnj966  31335  bnj1442  31438  erdszelem9  31502  erdszelem10  31503  txpconn  31535  txsconnlem  31543  msubval  31743  mvhval  31752  msubvrs  31778  brtpid1  31922  brtpid2  31923  brtpid3  31924  brtp  31959  dfpo2  31965  br8  31966  br6  31967  br4  31968  dfdm5  31994  dfrn5  31995  elima4  31997  fv1stcnv  31998  fv2ndcnv  31999  brtxp  32306  brpprod  32311  brpprod3b  32313  brsset  32315  brtxpsd  32320  dffun10  32340  elfuns  32341  brcart  32358  brimg  32363  brapply  32364  brcup  32365  brcap  32366  brsuccf  32367  brrestrict  32375  dfrecs2  32376  dfrdg4  32377  fvtransport  32458  brcolinear2  32484  colineardim1  32487  brsegle  32534  fvline  32570  ellines  32578  filnetlem3  32694  bj-inftyexpiinv  33410  bj-inftyexpidisj  33412  bj-elccinfty  33416  bj-minftyccb  33427  finxpreclem2  33541  finxp0  33542  finxp1o  33543  finxpreclem3  33544  finxpreclem4  33545  finxpreclem5  33546  finxpreclem6  33547  cnfin0  33554  poimirlem9  33729  poimirlem15  33735  poimirlem17  33737  poimirlem20  33740  poimirlem24  33744  poimirlem28  33748  mblfinlem2  33758  heiborlem6  33924  heiborlem7  33925  heiborlem8  33926  grposnOLD  33990  rngosn3  34032  gidsn  34060  zrdivrng  34061  brxrn  34447  br1cossxrnres  34509  dvhvaddval  36869  dvhvscaval  36878  dibglbN  36945  dihglbcpreN  37079  dihmeetlem4preN  37085  dihmeetlem13N  37098  hdmapfval  37606  elcnvlem  38405  cotrintab  38419  elimaint  38438  snhesn  38578  projf1o  39873  dvnprodlem1  40639  dvnprodlem2  40640  sge0xp  41123  hoicvr  41242  hoicvrrex  41250  hoidmv1le  41288  hoi2toco  41301  ovnlecvr2  41304  ovolval5lem2  41347  setsidel  41919  opeliun2xp  42677  lmod1lem2  42843  lmod1lem3  42844  lmod1zr  42848  zlmodzxznm  42852  zlmodzxzldeplem  42853