Theorem opex 5450

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 5274. (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 4601	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1156	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5414	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5302	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2862	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

This proof depends on syntax axioms:   ∧ w3a 1103   ∈ wcel 2146  {cab 2744  Vcvv 3458  {csn 4594  {cpr 4596  ⟨cop 4600

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-un 3913  df-in 3915  df-ss 3925  df-sn 4595  df-pr 4597  df-op 4601

This theorem is used by:  otex  5452  brv  5459  otth2  5470  otthg  5472  sbcop1  5475  oteqex2  5487  oteqex  5488  snopeqop  5494  propeqop  5495  propssopi  5496  euop2  5500  brsnop  5511  brtp  5512  opabidw  5513  opabid  5514  elopab  5516  rexopabb  5517  opabn0  5543  opeliunxp  5733  opeliun2xp  5734  elvvv  5742  opbrop  5764  relsnopg  5795  xpiindi  5826  raliunxp  5830  idrefALT  6118  intirr  6123  xpnz  6161  dmsnn0  6213  dmsnopg  6219  cnvcnvsn  6225  op2ndb  6233  opswap  6235  cnviin  6294  reuop  6301  dfpo2  6304  funopg  6577  dffv2  6983  fsn  7138  f1o2sn  7145  idref  7149  funsndifnop  7155  fmptsng  7173  fmptsnd  7174  fvsng  7185  resfunexg  7220  fveqf1o  7311  fliftel  7318  fliftel1  7319  oprabidw  7454  oprabid  7455  dfoprab2  7481  oprabv  7483  rnoprab  7528  eloprabga  7532  ot1stg  8009  ot2ndg  8010  ot3rdg  8011  fo1st  8015  fo2nd  8016  br1steqg  8017  br2ndeqg  8018  opiota  8065  eloprabi  8069  mposn  8107  fpar  8120  fsplitfpar  8122  opco1  8127  opco2  8128  frxp  8131  xporderlem  8132  fnwelem  8136  fvproj  8139  fimaproj  8140  xpord2lem  8147  xpord2pred  8150  xpord2indlem  8152  frxp3  8156  mpoxopoveq  8224  brtpos  8240  dmtpos  8243  rntpos  8244  tpostpos  8251  tfrlem11  8384  seqomlem1  8446  seqomlem3  8448  seqomlem4  8449  omeu  8579  naddcllem  8671  iiner  8796  xpsnen  9059  xpcomco  9065  xpassen  9069  xpmapenlem  9142  dif1en  9156  unxpdomlem1  9226  inlresf  9919  inrresf  9921  djur  9924  djuss  9925  djuun  9931  1stinl  9932  2ndinl  9933  1stinr  9934  2ndinr  9935  fseqenlem2  10028  dju1dif  10175  fpwwe  10649  addpipq2  10939  addpqnq  10941  mulpipq2  10942  mulpqnq  10944  ordpipq  10945  prlem934  11036  addcnsr  11138  mulcnsr  11139  ltresr  11143  addcnsrec  11146  mulcnsrec  11147  axcnre  11167  om2uzrdg  14012  uzrdg0i  14015  uzrdgsuci  14016  hashfun  14494  wrdexb  14582  s1len  14665  s1nz  14666  s111  14675  wrdlen2i  15005  brintclab  15064  fsumcnv  15850  fprodcnv  16063  ruclem1  16312  ruclem4  16315  eucalgval2  16664  crth  16862  phimullem  16863  setsval  17252  setsdm  17255  setsfun  17256  setsfun0  17257  setsexstruct2  17260  setsres  17263  setscom  17265  strfv  17288  setsid  17292  imasaddfnlem  17607  imasaddvallem  17608  imasvscafn  17616  idfuval  17958  cofuval  17964  resfval  17974  resfval2  17975  elhoma  18114  embedsetcestrclem  18238  xpcco  18264  xpcid  18270  1stfval  18272  2ndfval  18275  prfval  18280  prf1  18281  prf2  18283  evlfval  18298  curfval  18304  curf1  18306  curfcl  18313  hofval  18333  intopsn  18737  mgm1  18741  sgrp1  18816  mnd1  18868  mnd1id  18869  grpss  19052  grp1  19144  symg2bas  19494  efgmval  19813  efgi  19820  efgi2  19826  frgpnabllem1  19974  frgpnabllem2  19975  ring1  20426  rngqiprngimfv  21475  rngqiprngimf1  21477  opsrtoslem2  22244  mat1dimelbas  22665  mat1dimbas  22666  mat1dimscm  22669  mat1dimmul  22670  mat1f1o  22672  mat1rhmelval  22674  mvmulfval  22736  m2detleib  22825  txcnp  23814  upxp  23817  uptx  23819  txdis1cn  23829  hauseqlcld  23840  txlm  23842  xkoinjcn  23881  txflf  24200  qustgplem  24315  ucnima  24474  ucnprima  24475  fmucndlem  24484  imasdsf1olem  24567  cnheiborlem  25150  ovollb2lem  25684  ovolctb  25686  ovolshftlem1  25705  ovolscalem1  25709  ovolicc1  25712  ioombl1lem3  25756  ioombl1lem4  25757  ioorval  25770  dyadval  25788  mbfimaopnlem  25851  limccnp2  26088  addsval  28192  mulsval  28339  precsexlem1  28437  precsexlem2  28438  precsexlem3  28439  om2noseqrdg  28534  noseqrdg0  28537  noseqrdgsuc  28538  brbtwn  29286  brcgr  29287  eengbas  29368  ebtwntg  29369  ecgrtg  29370  elntg  29371  structvtxval  29408  structgrssvtx  29411  structgrssiedg  29412  gropd  29418  isuhgrop  29457  uhgrunop  29462  upgrop  29481  upgr0eop  29501  upgrunop  29506  umgrunop  29508  isuspgrop  29548  isusgrop  29549  ausgrusgrb  29552  usgr0eop  29633  griedg0ssusgr  29652  uhgrspanop  29683  uhgrspan1  29690  upgrres  29693  umgrres  29694  usgrres  29695  upgrres1  29700  umgrres1  29701  usgrres1  29702  usgrexi  29828  cusgrexi  29830  cffldtocusgr  29834  cusgrres  29835  vtxdgop  29857  umgr2v2e  29912  wlkp1lem2  30059  wlkswwlksf1o  30265  wwlksnext  30279  eupth2eucrct  30605  eupthvdres  30623  konigsbergumgr  30639  numclwwlk1lem2fv  30744  numclwlk1lem1  30757  ex-br  30819  ex-fpar  30850  cnnvg  31067  cnnvs  31069  cnnvnm  31070  h2hva  31363  h2hsm  31364  h2hnm  31365  hhssva  31646  hhsssm  31647  hhssnm  31648  hhshsslem1  31656  br8d  32990  xppreima2  33033  aciunf1lem  33044  ofpreima  33047  rlocaddval  33620  rlocmulval  33621  linds2eq  33725  selvply1rhmlema  33939  selvply1rhmlem1  33941  selvply1rhmlem2  33942  smatrcl  34217  smatlem  34218  txomap  34255  qtophaus  34257  hgt750lemb  35075  bnj97  35286  bnj553  35318  bnj966  35364  bnj1442  35469  erdszelem9  35712  erdszelem10  35713  txpconn  35745  txsconnlem  35753  goel  35860  goeleq12bg  35862  gonafv  35863  gonanegoal  35865  sat1el2xp  35892  fmlaomn0  35903  gonan0  35905  goaln0  35906  gonarlem  35907  gonar  35908  goalrlem  35909  goalr  35910  fmla0disjsuc  35911  fmlasucdisj  35912  satffunlem  35914  satffunlem1lem1  35915  satffunlem2lem1  35917  satfv0fvfmla0  35926  sategoelfvb  35932  prv1n  35944  msubval  36038  mvhval  36047  msubvrs  36073  brtpid1  36234  brtpid2  36235  brtpid3  36236  br8  36269  br6  36270  br4  36271  dfdm5  36286  dfrn5  36287  elima4  36289  fv1stcnv  36290  fv2ndcnv  36291  brtxp  36391  brpprod  36396  brpprod3b  36398  brsset  36400  brtxpsd  36405  dffun10  36425  elfuns  36426  brcart  36443  brimg  36448  brapply  36449  brcup  36450  brcap  36451  lemsuccf  36452  brrestrict  36462  dfrecs2  36463  dfrdg4  36464  fvtransport  36545  brcolinear2  36571  colineardim1  36574  brsegle  36621  fvline  36657  ellines  36665  nmulprop  36703  filnetlem3  36932  bj-inftyexpitaufo  37887  bj-inftyexpitaudisj  37890  bj-inftyexpiinv  37893  bj-inftyexpidisj  37895  bj-elccinfty  37899  bj-minftyccb  37910  finxpreclem2  38077  finxp0  38078  finxp1o  38079  finxpreclem3  38080  finxpreclem4  38081  finxpreclem5  38082  finxpreclem6  38083  poimirlem9  38321  poimirlem15  38327  poimirlem17  38329  poimirlem20  38332  poimirlem24  38336  poimirlem28  38340  mblfinlem2  38350  heiborlem6  38508  heiborlem7  38509  heiborlem8  38510  grposnOLD  38574  rngosn3  38616  gidsn  38644  zrdivrng  38645  brxrn  39073  ecxrn2  39098  br1cossxrnres  39228  dvhvaddval  41905  dvhvscaval  41914  dibglbN  41981  dihglbcpreN  42115  dihmeetlem4preN  42121  dihmeetlem13N  42134  hdmapfval  42642  elcnvlem  44368  cotrintab  44381  elimaint  44416  snhesn  44553  nregmodellem  45766  projf1o  45955  dvnprodlem1  46701  dvnprodlem2  46702  sge0xp  47184  hoicvr  47303  hoicvrrex  47311  hoidmv1le  47349  hoi2toco  47362  ovnlecvr2  47365  ovolval5lem2  47408  fsetsnf1  47830  setsidel  48166  prproropf1olem3  48295  prproropf1olem4  48296  prproropreud  48299  isisubgr  48668  ushggricedg  48733  gpgusgralem  48862  gpgvtxedg0  48869  gpgvtxedg1  48870  gpg5nbgrvtx03starlem1  48874  gpg5nbgrvtx03starlem2  48875  gpg5nbgrvtx03starlem3  48876  gpg5nbgrvtx13starlem1  48877  gpg5nbgrvtx13starlem2  48878  gpg5nbgrvtx13starlem3  48879  gpg3nbgrvtx0  48882  gpg3nbgrvtx0ALT  48883  gpg3nbgrvtx1  48884  gpg5nbgrvtx03star  48886  gpg5nbgr3star  48887  gpg3kgrtriex  48895  gpgprismgr4cycllem2  48902  gpgprismgr4cycllem6  48906  gpgprismgr4cycllem7  48907  gpgprismgr4cycllem10  48910  gpg5edgnedg  48936  lmod1lem2  49309  lmod1lem3  49310  lmod1zr  49314  zlmodzxznm  49318  zlmodzxzldeplem  49319  rrx2xpref1o  49539  line2x  49575  inlinecirc02plem  49607  iinxp  49650  ovsng  49677  eloprab1st2nd  49687  tposid  49704  tposidres  49705  initc  49910  rescofuf  49912  idfurcl  49917  imaf1hom  49927  oppffn  49943  oppfvalg  49945  swapfval  50081  swapf1a  50088  swapf2a  50090  swapf1  50091  swapf2  50093  fucofvalg  50137  fucofval  50138  fucofvalne  50144  fuco21  50155  fucof21  50166  prcofvalg  50195  prcofvala  50196  prcofval  50197  thincciso  50272  setc1ocofval  50313  functermceu  50329  termcfuncval  50351  fucterm  50361  0fucterm  50362  relran  50443  ranval3  50450  ranrcl4lem  50457  ranup  50461  initocmd  50488