Theorem opex 5435

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 5260. (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 4592	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1154	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5399	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5286	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2861	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1101   ∈ wcel 2145  {cab 2743  Vcvv 3457  {csn 4585  {cpr 4587  ⟨cop 4591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5250  ax-pr 5394

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-un 3912  df-in 3914  df-ss 3924  df-sn 4586  df-pr 4588  df-op 4592

This theorem is referenced by:  otex  5437  brv  5444  otth2  5455  otthg  5457  sbcop1  5460  oteqex2  5472  oteqex  5473  snopeqop  5479  propeqop  5480  propssopi  5481  euop2  5485  brsnop  5496  brtp  5497  opabidw  5498  opabid  5499  elopab  5501  rexopabb  5502  opabn0  5528  opeliunxp  5718  opeliun2xp  5719  elvvv  5727  opbrop  5749  relsnopg  5780  xpiindi  5811  raliunxp  5815  idrefALT  6103  intirr  6108  xpnz  6147  dmsnn0  6197  dmsnopg  6203  cnvcnvsn  6209  op2ndb  6217  opswap  6219  cnviin  6276  reuop  6283  dfpo2  6286  funopg  6559  dffv2  6966  fsn  7121  f1o2sn  7128  idref  7132  funsndifnop  7138  fmptsng  7156  fmptsnd  7157  fvsng  7168  resfunexg  7203  fveqf1o  7290  fliftel  7297  fliftel1  7298  oprabidw  7431  oprabid  7432  dfoprab2  7458  oprabv  7460  rnoprab  7505  eloprabga  7509  ot1stg  7988  ot2ndg  7989  ot3rdg  7990  fo1st  7994  fo2nd  7995  br1steqg  7996  br2ndeqg  7997  opiota  8044  eloprabi  8048  mposn  8086  fpar  8099  fsplitfpar  8101  opco1  8106  opco2  8107  frxp  8110  xporderlem  8111  fnwelem  8115  fvproj  8118  fimaproj  8119  xpord2lem  8126  xpord2pred  8129  xpord2indlem  8131  frxp3  8135  mpoxopoveq  8203  brtpos  8219  dmtpos  8222  rntpos  8223  tpostpos  8230  tfrlem11  8363  seqomlem1  8425  seqomlem3  8427  seqomlem4  8428  omeu  8558  naddcllem  8650  iiner  8775  xpsnen  9037  xpcomco  9043  xpassen  9047  xpmapenlem  9120  dif1en  9134  unxpdomlem1  9204  inlresf  9888  inrresf  9890  djur  9893  djuss  9894  djuun  9900  1stinl  9901  2ndinl  9902  1stinr  9903  2ndinr  9904  fseqenlem2  9997  dju1dif  10144  fpwwe  10619  addpipq2  10909  addpqnq  10911  mulpipq2  10912  mulpqnq  10914  ordpipq  10915  prlem934  11006  addcnsr  11108  mulcnsr  11109  ltresr  11113  addcnsrec  11116  mulcnsrec  11117  axcnre  11137  om2uzrdg  13980  uzrdg0i  13983  uzrdgsuci  13984  hashfun  14462  wrdexb  14550  s1len  14632  s1nz  14633  s111  14641  wrdlen2i  14967  brintclab  15026  fsumcnv  15812  fprodcnv  16025  ruclem1  16275  ruclem4  16278  eucalgval2  16627  crth  16825  phimullem  16826  setsval  17215  setsdm  17218  setsfun  17219  setsfun0  17220  setsexstruct2  17223  setsres  17226  setscom  17228  strfv  17251  setsid  17255  imasaddfnlem  17570  imasaddvallem  17571  imasvscafn  17579  idfuval  17921  cofuval  17927  resfval  17937  resfval2  17938  elhoma  18077  embedsetcestrclem  18201  xpcco  18227  xpcid  18233  1stfval  18235  2ndfval  18238  prfval  18243  prf1  18244  prf2  18246  evlfval  18261  curfval  18267  curf1  18269  curfcl  18276  hofval  18296  intopsn  18700  mgm1  18704  sgrp1  18775  mnd1  18825  mnd1id  18826  grpss  19009  grp1  19101  symg2bas  19451  efgmval  19770  efgi  19777  efgi2  19783  frgpnabllem1  19931  frgpnabllem2  19932  ring1  20381  rngqiprngimfv  21397  rngqiprngimf1  21399  opsrtoslem2  22164  mat1dimelbas  22585  mat1dimbas  22586  mat1dimscm  22589  mat1dimmul  22590  mat1f1o  22592  mat1rhmelval  22594  mvmulfval  22656  m2detleib  22745  txcnp  23734  upxp  23737  uptx  23739  txdis1cn  23749  hauseqlcld  23760  txlm  23762  xkoinjcn  23801  txflf  24120  qustgplem  24235  ucnima  24394  ucnprima  24395  fmucndlem  24404  imasdsf1olem  24487  cnheiborlem  25070  ovollb2lem  25604  ovolctb  25606  ovolshftlem1  25625  ovolscalem1  25629  ovolicc1  25632  ioombl1lem3  25676  ioombl1lem4  25677  ioorval  25690  dyadval  25708  mbfimaopnlem  25771  limccnp2  26008  addsval  28109  mulsval  28256  precsexlem1  28354  precsexlem2  28355  precsexlem3  28356  om2noseqrdg  28451  noseqrdg0  28454  noseqrdgsuc  28455  brbtwn  29154  brcgr  29155  eengbas  29236  ebtwntg  29237  ecgrtg  29238  elntg  29239  structvtxval  29276  structgrssvtx  29279  structgrssiedg  29280  gropd  29286  isuhgrop  29325  uhgrunop  29330  upgrop  29349  upgr0eop  29369  upgrunop  29374  umgrunop  29376  isuspgrop  29416  isusgrop  29417  ausgrusgrb  29420  usgr0eop  29501  griedg0ssusgr  29520  uhgrspanop  29551  uhgrspan1  29558  upgrres  29561  umgrres  29562  usgrres  29563  upgrres1  29568  umgrres1  29569  usgrres1  29570  usgrexi  29696  cusgrexi  29698  cffldtocusgr  29702  cusgrres  29703  vtxdgop  29725  umgr2v2e  29780  wlkp1lem2  29927  wlkswwlksf1o  30133  wwlksnext  30147  eupth2eucrct  30473  eupthvdres  30491  konigsbergumgr  30507  numclwwlk1lem2fv  30612  numclwlk1lem1  30625  ex-br  30687  ex-fpar  30718  cnnvg  30935  cnnvs  30937  cnnvnm  30938  h2hva  31231  h2hsm  31232  h2hnm  31233  hhssva  31514  hhsssm  31515  hhssnm  31516  hhshsslem1  31524  br8d  32861  xppreima2  32904  aciunf1lem  32915  ofpreima  32918  rlocaddval  33497  rlocmulval  33498  linds2eq  33605  selvply1rhmlema  33820  selvply1rhmlem1  33822  selvply1rhmlem2  33823  smatrcl  34098  smatlem  34099  txomap  34136  qtophaus  34138  hgt750lemb  34955  bnj97  35166  bnj553  35198  bnj966  35244  bnj1442  35349  erdszelem9  35557  erdszelem10  35558  txpconn  35590  txsconnlem  35598  goel  35705  goeleq12bg  35707  gonafv  35708  gonanegoal  35710  sat1el2xp  35737  fmlaomn0  35748  gonan0  35750  goaln0  35751  gonarlem  35752  gonar  35753  goalrlem  35754  goalr  35755  fmla0disjsuc  35756  fmlasucdisj  35757  satffunlem  35759  satffunlem1lem1  35760  satffunlem2lem1  35762  satfv0fvfmla0  35771  sategoelfvb  35777  prv1n  35789  msubval  35883  mvhval  35892  msubvrs  35918  brtpid1  36079  brtpid2  36080  brtpid3  36081  br8  36114  br6  36115  br4  36116  dfdm5  36131  dfrn5  36132  elima4  36134  fv1stcnv  36135  fv2ndcnv  36136  brtxp  36236  brpprod  36241  brpprod3b  36243  brsset  36245  brtxpsd  36250  dffun10  36270  elfuns  36271  brcart  36288  brimg  36293  brapply  36294  brcup  36295  brcap  36296  lemsuccf  36297  brrestrict  36307  dfrecs2  36308  dfrdg4  36309  fvtransport  36390  brcolinear2  36416  colineardim1  36419  brsegle  36466  fvline  36502  ellines  36510  nmulprop  36548  filnetlem3  36748  bj-inftyexpitaufo  37701  bj-inftyexpitaudisj  37704  bj-inftyexpiinv  37707  bj-inftyexpidisj  37709  bj-elccinfty  37713  bj-minftyccb  37724  finxpreclem2  37891  finxp0  37892  finxp1o  37893  finxpreclem3  37894  finxpreclem4  37895  finxpreclem5  37896  finxpreclem6  37897  poimirlem9  38135  poimirlem15  38141  poimirlem17  38143  poimirlem20  38146  poimirlem24  38150  poimirlem28  38154  mblfinlem2  38164  heiborlem6  38322  heiborlem7  38323  heiborlem8  38324  grposnOLD  38388  rngosn3  38430  gidsn  38458  zrdivrng  38459  brxrn  38889  ecxrn2  38914  br1cossxrnres  39044  dvhvaddval  41721  dvhvscaval  41730  dibglbN  41797  dihglbcpreN  41931  dihmeetlem4preN  41937  dihmeetlem13N  41950  hdmapfval  42458  elcnvlem  44184  cotrintab  44197  elimaint  44232  snhesn  44369  nregmodellem  45584  projf1o  45773  dvnprodlem1  46519  dvnprodlem2  46520  sge0xp  47002  hoicvr  47121  hoicvrrex  47129  hoidmv1le  47167  hoi2toco  47180  ovnlecvr2  47183  ovolval5lem2  47226  fsetsnf1  47645  setsidel  47981  prproropf1olem3  48110  prproropf1olem4  48111  prproropreud  48114  isisubgr  48483  ushggricedg  48548  gpgusgralem  48677  gpgvtxedg0  48684  gpgvtxedg1  48685  gpg5nbgrvtx03starlem1  48689  gpg5nbgrvtx03starlem2  48690  gpg5nbgrvtx03starlem3  48691  gpg5nbgrvtx13starlem1  48692  gpg5nbgrvtx13starlem2  48693  gpg5nbgrvtx13starlem3  48694  gpg3nbgrvtx0  48697  gpg3nbgrvtx0ALT  48698  gpg3nbgrvtx1  48699  gpg5nbgrvtx03star  48701  gpg5nbgr3star  48702  gpg3kgrtriex  48710  gpgprismgr4cycllem2  48717  gpgprismgr4cycllem6  48721  gpgprismgr4cycllem7  48722  gpgprismgr4cycllem10  48725  gpg5edgnedg  48751  lmod1lem2  49120  lmod1lem3  49121  lmod1zr  49125  zlmodzxznm  49129  zlmodzxzldeplem  49130  rrx2xpref1o  49350  line2x  49386  inlinecirc02plem  49418  iinxp  49461  ovsng  49488  eloprab1st2nd  49498  tposid  49515  tposidres  49516  initc  49721  rescofuf  49723  idfurcl  49728  imaf1hom  49738  oppffn  49754  oppfvalg  49756  swapfval  49892  swapf1a  49899  swapf2a  49901  swapf1  49902  swapf2  49904  fucofvalg  49948  fucofval  49949  fucofvalne  49955  fuco21  49966  fucof21  49977  prcofvalg  50006  prcofvala  50007  prcofval  50008  thincciso  50083  setc1ocofval  50124  functermceu  50140  termcfuncval  50162  fucterm  50172  0fucterm  50173  relran  50254  ranval3  50261  ranrcl4lem  50268  ranup  50272  initocmd  50299