Theorem opex 5411

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 4575	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1139	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5375	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5263	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2833	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1087   ∈ wcel 2114  {cab 2715  Vcvv 3430  {csn 4568  {cpr 4570  ⟨cop 4574

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 2709  ax-sep 5231  ax-pr 5370

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 2716  df-cleq 2729  df-clel 2812  df-rab 3391  df-v 3432  df-un 3895  df-in 3897  df-ss 3907  df-sn 4569  df-pr 4571  df-op 4575

This theorem is referenced by:  otex  5413  brv  5420  otth2  5431  otthg  5433  sbcop1  5436  oteqex2  5447  oteqex  5448  snopeqop  5454  propeqop  5455  propssopi  5456  euop2  5460  brsnop  5470  brtp  5471  opabidw  5472  opabid  5473  elopab  5475  rexopabb  5476  opabn0  5501  opeliunxp  5691  opeliun2xp  5692  elvvv  5700  opbrop  5722  relsnopg  5752  xpiindi  5784  raliunxp  5788  idrefALT  6070  intirr  6075  xpnz  6117  dmsnn0  6165  dmsnopg  6171  cnvcnvsn  6177  op2ndb  6185  opswap  6187  cnviin  6244  reuop  6251  dfpo2  6254  funopg  6526  dffv2  6929  fsn  7082  f1o2sn  7089  idref  7093  funsndifnop  7098  fmptsng  7116  fmptsnd  7117  fvsng  7128  resfunexg  7163  fveqf1o  7250  fliftel  7257  fliftel1  7258  oprabidw  7391  oprabid  7392  dfoprab2  7418  oprabv  7420  rnoprab  7465  eloprabga  7469  ot1stg  7949  ot2ndg  7950  ot3rdg  7951  fo1st  7955  fo2nd  7956  br1steqg  7957  br2ndeqg  7958  opiota  8005  eloprabi  8009  mposn  8046  fpar  8059  fsplitfpar  8061  opco1  8066  opco2  8067  frxp  8069  xporderlem  8070  fnwelem  8074  fvproj  8077  fimaproj  8078  xpord2lem  8085  xpord2pred  8088  xpord2indlem  8090  frxp3  8094  mpoxopoveq  8162  brtpos  8178  dmtpos  8181  rntpos  8182  tpostpos  8189  tfrlem11  8320  seqomlem1  8382  seqomlem3  8384  seqomlem4  8385  omeu  8513  naddcllem  8605  iiner  8729  xpsnen  8992  xpcomco  8998  xpassen  9002  xpmapenlem  9075  dif1en  9089  unxpdomlem1  9159  inlresf  9829  inrresf  9831  djur  9834  djuss  9835  djuun  9841  1stinl  9842  2ndinl  9843  1stinr  9844  2ndinr  9845  fseqenlem2  9938  dju1dif  10086  fpwwe  10560  addpipq2  10850  addpqnq  10852  mulpipq2  10853  mulpqnq  10855  ordpipq  10856  prlem934  10947  addcnsr  11049  mulcnsr  11050  ltresr  11054  addcnsrec  11057  mulcnsrec  11058  axcnre  11078  om2uzrdg  13909  uzrdg0i  13912  uzrdgsuci  13913  hashfun  14390  wrdexb  14478  s1len  14560  s1nz  14561  s111  14569  wrdlen2i  14895  brintclab  14954  fsumcnv  15726  fprodcnv  15939  ruclem1  16189  ruclem4  16192  eucalgval2  16541  crth  16739  phimullem  16740  setsval  17128  setsdm  17131  setsfun  17132  setsfun0  17133  setsexstruct2  17136  setsres  17139  setscom  17141  strfv  17164  setsid  17168  imasaddfnlem  17483  imasaddvallem  17484  imasvscafn  17492  idfuval  17834  cofuval  17840  resfval  17850  resfval2  17851  elhoma  17990  embedsetcestrclem  18114  xpcco  18140  xpcid  18146  1stfval  18148  2ndfval  18151  prfval  18156  prf1  18157  prf2  18159  evlfval  18174  curfval  18180  curf1  18182  curfcl  18189  hofval  18209  intopsn  18613  mgm1  18617  sgrp1  18688  mnd1  18738  mnd1id  18739  grpss  18921  grp1  19014  symg2bas  19359  efgmval  19678  efgi  19685  efgi2  19691  frgpnabllem1  19839  frgpnabllem2  19840  ring1  20282  rngqiprngimfv  21288  rngqiprngimf1  21290  opsrtoslem2  22044  mat1dimelbas  22446  mat1dimbas  22447  mat1dimscm  22450  mat1dimmul  22451  mat1f1o  22453  mat1rhmelval  22455  mvmulfval  22517  m2detleib  22606  txcnp  23595  upxp  23598  uptx  23600  txdis1cn  23610  hauseqlcld  23621  txlm  23623  xkoinjcn  23662  txflf  23981  qustgplem  24096  ucnima  24255  ucnprima  24256  fmucndlem  24265  imasdsf1olem  24348  cnheiborlem  24931  ovollb2lem  25465  ovolctb  25467  ovolshftlem1  25486  ovolscalem1  25490  ovolicc1  25493  ioombl1lem3  25537  ioombl1lem4  25538  ioorval  25551  dyadval  25569  mbfimaopnlem  25632  limccnp2  25869  addsval  27968  mulsval  28115  precsexlem1  28213  precsexlem2  28214  precsexlem3  28215  om2noseqrdg  28310  noseqrdg0  28313  noseqrdgsuc  28314  brbtwn  28982  brcgr  28983  eengbas  29064  ebtwntg  29065  ecgrtg  29066  elntg  29067  structvtxval  29104  structgrssvtx  29107  structgrssiedg  29108  gropd  29114  isuhgrop  29153  uhgrunop  29158  upgrop  29177  upgr0eop  29197  upgrunop  29202  umgrunop  29204  isuspgrop  29244  isusgrop  29245  ausgrusgrb  29248  usgr0eop  29329  griedg0ssusgr  29348  uhgrspanop  29379  uhgrspan1  29386  upgrres  29389  umgrres  29390  usgrres  29391  upgrres1  29396  umgrres1  29397  usgrres1  29398  usgrexi  29524  cusgrexi  29526  cffldtocusgr  29530  cffldtocusgrOLD  29531  cusgrres  29532  vtxdgop  29554  umgr2v2e  29609  wlkp1lem2  29756  wlkswwlksf1o  29962  wwlksnext  29976  eupth2eucrct  30302  eupthvdres  30320  konigsbergumgr  30336  numclwwlk1lem2fv  30441  numclwlk1lem1  30454  ex-br  30516  ex-fpar  30547  cnnvg  30764  cnnvs  30766  cnnvnm  30767  h2hva  31060  h2hsm  31061  h2hnm  31062  hhssva  31343  hhsssm  31344  hhssnm  31345  hhshsslem1  31353  br8d  32696  xppreima2  32739  aciunf1lem  32750  ofpreima  32753  rlocaddval  33344  rlocmulval  33345  linds2eq  33456  smatrcl  33956  smatlem  33957  txomap  33994  qtophaus  33996  hgt750lemb  34816  bnj97  35024  bnj553  35056  bnj966  35102  bnj1442  35207  erdszelem9  35397  erdszelem10  35398  txpconn  35430  txsconnlem  35438  goel  35545  goeleq12bg  35547  gonafv  35548  gonanegoal  35550  sat1el2xp  35577  fmlaomn0  35588  gonan0  35590  goaln0  35591  gonarlem  35592  gonar  35593  goalrlem  35594  goalr  35595  fmla0disjsuc  35596  fmlasucdisj  35597  satffunlem  35599  satffunlem1lem1  35600  satffunlem2lem1  35602  satfv0fvfmla0  35611  sategoelfvb  35617  prv1n  35629  msubval  35723  mvhval  35732  msubvrs  35758  brtpid1  35919  brtpid2  35920  brtpid3  35921  br8  35954  br6  35955  br4  35956  dfdm5  35971  dfrn5  35972  elima4  35974  fv1stcnv  35975  fv2ndcnv  35976  brtxp  36076  brpprod  36081  brpprod3b  36083  brsset  36085  brtxpsd  36090  dffun10  36110  elfuns  36111  brcart  36128  brimg  36133  brapply  36134  brcup  36135  brcap  36136  lemsuccf  36137  brrestrict  36147  dfrecs2  36148  dfrdg4  36149  fvtransport  36230  brcolinear2  36256  colineardim1  36259  brsegle  36306  fvline  36342  ellines  36350  filnetlem3  36578  bj-inftyexpitaufo  37532  bj-inftyexpitaudisj  37535  bj-inftyexpiinv  37538  bj-inftyexpidisj  37540  bj-elccinfty  37544  bj-minftyccb  37555  finxpreclem2  37720  finxp0  37721  finxp1o  37722  finxpreclem3  37723  finxpreclem4  37724  finxpreclem5  37725  finxpreclem6  37726  poimirlem9  37964  poimirlem15  37970  poimirlem17  37972  poimirlem20  37975  poimirlem24  37979  poimirlem28  37983  mblfinlem2  37993  heiborlem6  38151  heiborlem7  38152  heiborlem8  38153  grposnOLD  38217  rngosn3  38259  gidsn  38287  zrdivrng  38288  brxrn  38718  ecxrn2  38743  br1cossxrnres  38873  dvhvaddval  41550  dvhvscaval  41559  dibglbN  41626  dihglbcpreN  41760  dihmeetlem4preN  41766  dihmeetlem13N  41779  hdmapfval  42287  elcnvlem  44046  cotrintab  44059  elimaint  44094  snhesn  44231  nregmodellem  45461  projf1o  45644  dvnprodlem1  46392  dvnprodlem2  46393  sge0xp  46875  hoicvr  46994  hoicvrrex  47002  hoidmv1le  47040  hoi2toco  47053  ovnlecvr2  47056  ovolval5lem2  47099  fsetsnf1  47512  setsidel  47848  prproropf1olem3  47977  prproropf1olem4  47978  prproropreud  47981  isisubgr  48350  ushggricedg  48415  gpgusgralem  48544  gpgvtxedg0  48551  gpgvtxedg1  48552  gpg5nbgrvtx03starlem1  48556  gpg5nbgrvtx03starlem2  48557  gpg5nbgrvtx03starlem3  48558  gpg5nbgrvtx13starlem1  48559  gpg5nbgrvtx13starlem2  48560  gpg5nbgrvtx13starlem3  48561  gpg3nbgrvtx0  48564  gpg3nbgrvtx0ALT  48565  gpg3nbgrvtx1  48566  gpg5nbgrvtx03star  48568  gpg5nbgr3star  48569  gpg3kgrtriex  48577  gpgprismgr4cycllem2  48584  gpgprismgr4cycllem6  48588  gpgprismgr4cycllem7  48589  gpgprismgr4cycllem10  48592  gpg5edgnedg  48618  lmod1lem2  48976  lmod1lem3  48977  lmod1zr  48981  zlmodzxznm  48985  zlmodzxzldeplem  48986  rrx2xpref1o  49206  line2x  49242  inlinecirc02plem  49274  iinxp  49318  ovsng  49345  eloprab1st2nd  49355  tposid  49372  tposidres  49373  initc  49578  rescofuf  49580  idfurcl  49585  imaf1hom  49595  oppffn  49611  oppfvalg  49613  swapfval  49749  swapf1a  49756  swapf2a  49758  swapf1  49759  swapf2  49761  fucofvalg  49805  fucofval  49806  fucofvalne  49812  fuco21  49823  fucof21  49834  prcofvalg  49863  prcofvala  49864  prcofval  49865  thincciso  49940  setc1ocofval  49981  functermceu  49997  termcfuncval  50019  fucterm  50029  0fucterm  50030  relran  50111  ranval3  50118  ranrcl4lem  50125  ranup  50129  initocmd  50156