Theorem opex 5416

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.) Avoid ax-nul 5241. (Revised by GG, 6-Mar-2026.)

Assertion

Ref	Expression
opex	⊢ ⟨𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-op 4574	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1139	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5380	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5267	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2832	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1087   ∈ wcel 2114  {cab 2714  Vcvv 3429  {csn 4567  {cpr 4569  ⟨cop 4573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-un 3894  df-in 3896  df-ss 3906  df-sn 4568  df-pr 4570  df-op 4574

This theorem is referenced by:  otex  5418  brv  5425  otth2  5436  otthg  5438  sbcop1  5441  oteqex2  5453  oteqex  5454  snopeqop  5460  propeqop  5461  propssopi  5462  euop2  5466  brsnop  5477  brtp  5478  opabidw  5479  opabid  5480  elopab  5482  rexopabb  5483  opabn0  5508  opeliunxp  5698  opeliun2xp  5699  elvvv  5707  opbrop  5729  relsnopg  5759  xpiindi  5790  raliunxp  5794  idrefALT  6076  intirr  6081  xpnz  6123  dmsnn0  6171  dmsnopg  6177  cnvcnvsn  6183  op2ndb  6191  opswap  6193  cnviin  6250  reuop  6257  dfpo2  6260  funopg  6532  dffv2  6935  fsn  7088  f1o2sn  7095  idref  7099  funsndifnop  7105  fmptsng  7123  fmptsnd  7124  fvsng  7135  resfunexg  7170  fveqf1o  7257  fliftel  7264  fliftel1  7265  oprabidw  7398  oprabid  7399  dfoprab2  7425  oprabv  7427  rnoprab  7472  eloprabga  7476  ot1stg  7956  ot2ndg  7957  ot3rdg  7958  fo1st  7962  fo2nd  7963  br1steqg  7964  br2ndeqg  7965  opiota  8012  eloprabi  8016  mposn  8053  fpar  8066  fsplitfpar  8068  opco1  8073  opco2  8074  frxp  8076  xporderlem  8077  fnwelem  8081  fvproj  8084  fimaproj  8085  xpord2lem  8092  xpord2pred  8095  xpord2indlem  8097  frxp3  8101  mpoxopoveq  8169  brtpos  8185  dmtpos  8188  rntpos  8189  tpostpos  8196  tfrlem11  8327  seqomlem1  8389  seqomlem3  8391  seqomlem4  8392  omeu  8520  naddcllem  8612  iiner  8736  xpsnen  8999  xpcomco  9005  xpassen  9009  xpmapenlem  9082  dif1en  9096  unxpdomlem1  9166  inlresf  9838  inrresf  9840  djur  9843  djuss  9844  djuun  9850  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  fseqenlem2  9947  dju1dif  10095  fpwwe  10569  addpipq2  10859  addpqnq  10861  mulpipq2  10862  mulpqnq  10864  ordpipq  10865  prlem934  10956  addcnsr  11058  mulcnsr  11059  ltresr  11063  addcnsrec  11066  mulcnsrec  11067  axcnre  11087  om2uzrdg  13918  uzrdg0i  13921  uzrdgsuci  13922  hashfun  14399  wrdexb  14487  s1len  14569  s1nz  14570  s111  14578  wrdlen2i  14904  brintclab  14963  fsumcnv  15735  fprodcnv  15948  ruclem1  16198  ruclem4  16201  eucalgval2  16550  crth  16748  phimullem  16749  setsval  17137  setsdm  17140  setsfun  17141  setsfun0  17142  setsexstruct2  17145  setsres  17148  setscom  17150  strfv  17173  setsid  17177  imasaddfnlem  17492  imasaddvallem  17493  imasvscafn  17501  idfuval  17843  cofuval  17849  resfval  17859  resfval2  17860  elhoma  17999  embedsetcestrclem  18123  xpcco  18149  xpcid  18155  1stfval  18157  2ndfval  18160  prfval  18165  prf1  18166  prf2  18168  evlfval  18183  curfval  18189  curf1  18191  curfcl  18198  hofval  18218  intopsn  18622  mgm1  18626  sgrp1  18697  mnd1  18747  mnd1id  18748  grpss  18930  grp1  19023  symg2bas  19368  efgmval  19687  efgi  19694  efgi2  19700  frgpnabllem1  19848  frgpnabllem2  19849  ring1  20291  rngqiprngimfv  21296  rngqiprngimf1  21298  opsrtoslem2  22034  mat1dimelbas  22436  mat1dimbas  22437  mat1dimscm  22440  mat1dimmul  22441  mat1f1o  22443  mat1rhmelval  22445  mvmulfval  22507  m2detleib  22596  txcnp  23585  upxp  23588  uptx  23590  txdis1cn  23600  hauseqlcld  23611  txlm  23613  xkoinjcn  23652  txflf  23971  qustgplem  24086  ucnima  24245  ucnprima  24246  fmucndlem  24255  imasdsf1olem  24338  cnheiborlem  24921  ovollb2lem  25455  ovolctb  25457  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  ioombl1lem3  25527  ioombl1lem4  25528  ioorval  25541  dyadval  25559  mbfimaopnlem  25622  limccnp2  25859  addsval  27954  mulsval  28101  precsexlem1  28199  precsexlem2  28200  precsexlem3  28201  om2noseqrdg  28296  noseqrdg0  28299  noseqrdgsuc  28300  brbtwn  28968  brcgr  28969  eengbas  29050  ebtwntg  29051  ecgrtg  29052  elntg  29053  structvtxval  29090  structgrssvtx  29093  structgrssiedg  29094  gropd  29100  isuhgrop  29139  uhgrunop  29144  upgrop  29163  upgr0eop  29183  upgrunop  29188  umgrunop  29190  isuspgrop  29230  isusgrop  29231  ausgrusgrb  29234  usgr0eop  29315  griedg0ssusgr  29334  uhgrspanop  29365  uhgrspan1  29372  upgrres  29375  umgrres  29376  usgrres  29377  upgrres1  29382  umgrres1  29383  usgrres1  29384  usgrexi  29510  cusgrexi  29512  cffldtocusgr  29516  cusgrres  29517  vtxdgop  29539  umgr2v2e  29594  wlkp1lem2  29741  wlkswwlksf1o  29947  wwlksnext  29961  eupth2eucrct  30287  eupthvdres  30305  konigsbergumgr  30321  numclwwlk1lem2fv  30426  numclwlk1lem1  30439  ex-br  30501  ex-fpar  30532  cnnvg  30749  cnnvs  30751  cnnvnm  30752  h2hva  31045  h2hsm  31046  h2hnm  31047  hhssva  31328  hhsssm  31329  hhssnm  31330  hhshsslem1  31338  br8d  32681  xppreima2  32724  aciunf1lem  32735  ofpreima  32738  rlocaddval  33329  rlocmulval  33330  linds2eq  33441  smatrcl  33940  smatlem  33941  txomap  33978  qtophaus  33980  hgt750lemb  34800  bnj97  35008  bnj553  35040  bnj966  35086  bnj1442  35191  erdszelem9  35381  erdszelem10  35382  txpconn  35414  txsconnlem  35422  goel  35529  goeleq12bg  35531  gonafv  35532  gonanegoal  35534  sat1el2xp  35561  fmlaomn0  35572  gonan0  35574  goaln0  35575  gonarlem  35576  gonar  35577  goalrlem  35578  goalr  35579  fmla0disjsuc  35580  fmlasucdisj  35581  satffunlem  35583  satffunlem1lem1  35584  satffunlem2lem1  35586  satfv0fvfmla0  35595  sategoelfvb  35601  prv1n  35613  msubval  35707  mvhval  35716  msubvrs  35742  brtpid1  35903  brtpid2  35904  brtpid3  35905  br8  35938  br6  35939  br4  35940  dfdm5  35955  dfrn5  35956  elima4  35958  fv1stcnv  35959  fv2ndcnv  35960  brtxp  36060  brpprod  36065  brpprod3b  36067  brsset  36069  brtxpsd  36074  dffun10  36094  elfuns  36095  brcart  36112  brimg  36117  brapply  36118  brcup  36119  brcap  36120  lemsuccf  36121  brrestrict  36131  dfrecs2  36132  dfrdg4  36133  fvtransport  36214  brcolinear2  36240  colineardim1  36243  brsegle  36290  fvline  36326  ellines  36334  filnetlem3  36562  bj-inftyexpitaufo  37516  bj-inftyexpitaudisj  37519  bj-inftyexpiinv  37522  bj-inftyexpidisj  37524  bj-elccinfty  37528  bj-minftyccb  37539  finxpreclem2  37706  finxp0  37707  finxp1o  37708  finxpreclem3  37709  finxpreclem4  37710  finxpreclem5  37711  finxpreclem6  37712  poimirlem9  37950  poimirlem15  37956  poimirlem17  37958  poimirlem20  37961  poimirlem24  37965  poimirlem28  37969  mblfinlem2  37979  heiborlem6  38137  heiborlem7  38138  heiborlem8  38139  grposnOLD  38203  rngosn3  38245  gidsn  38273  zrdivrng  38274  brxrn  38704  ecxrn2  38729  br1cossxrnres  38859  dvhvaddval  41536  dvhvscaval  41545  dibglbN  41612  dihglbcpreN  41746  dihmeetlem4preN  41752  dihmeetlem13N  41765  hdmapfval  42273  elcnvlem  44028  cotrintab  44041  elimaint  44076  snhesn  44213  nregmodellem  45443  projf1o  45626  dvnprodlem1  46374  dvnprodlem2  46375  sge0xp  46857  hoicvr  46976  hoicvrrex  46984  hoidmv1le  47022  hoi2toco  47035  ovnlecvr2  47038  ovolval5lem2  47081  fsetsnf1  47500  setsidel  47836  prproropf1olem3  47965  prproropf1olem4  47966  prproropreud  47969  isisubgr  48338  ushggricedg  48403  gpgusgralem  48532  gpgvtxedg0  48539  gpgvtxedg1  48540  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg3nbgrvtx0  48552  gpg3nbgrvtx0ALT  48553  gpg3nbgrvtx1  48554  gpg5nbgrvtx03star  48556  gpg5nbgr3star  48557  gpg3kgrtriex  48565  gpgprismgr4cycllem2  48572  gpgprismgr4cycllem6  48576  gpgprismgr4cycllem7  48577  gpgprismgr4cycllem10  48580  gpg5edgnedg  48606  lmod1lem2  48964  lmod1lem3  48965  lmod1zr  48969  zlmodzxznm  48973  zlmodzxzldeplem  48974  rrx2xpref1o  49194  line2x  49230  inlinecirc02plem  49262  iinxp  49306  ovsng  49333  eloprab1st2nd  49343  tposid  49360  tposidres  49361  initc  49566  rescofuf  49568  idfurcl  49573  imaf1hom  49583  oppffn  49599  oppfvalg  49601  swapfval  49737  swapf1a  49744  swapf2a  49746  swapf1  49747  swapf2  49749  fucofvalg  49793  fucofval  49794  fucofvalne  49800  fuco21  49811  fucof21  49822  prcofvalg  49851  prcofvala  49852  prcofval  49853  thincciso  49928  setc1ocofval  49969  functermceu  49985  termcfuncval  50007  fucterm  50017  0fucterm  50018  relran  50099  ranval3  50106  ranrcl4lem  50113  ranup  50117  initocmd  50144