Theorem opex 5439

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

This proof depends on syntax axioms:   ∧ w3a 1103   ∈ wcel 2145  {cab 2738  Vcvv 3450  {csn 4584  {cpr 4586  ⟨cop 4590

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 2147  ax-9 2155  ax-ext 2732  ax-sep 5251  ax-pr 5398

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  otex  5441  brv  5448  otth2  5459  otthg  5461  sbcop1  5464  oteqex2  5476  oteqex  5477  snopeqop  5483  propeqop  5484  propssopi  5485  euop2  5489  brsnop  5500  brtp  5501  opabidw  5502  opabid  5503  elopab  5505  rexopabb  5506  opabn0  5532  opeliunxp  5722  opeliun2xp  5723  elvvv  5731  opbrop  5753  relsnopg  5784  xpiindi  5815  raliunxp  5819  idrefALT  6107  intirr  6112  xpnz  6151  dmsnn0  6203  dmsnopg  6209  cnvcnvsn  6215  op2ndb  6223  opswap  6225  cnviin  6284  reuop  6291  dfpo2  6294  funopg  6567  dffv2  6973  fsn  7129  f1o2sn  7138  idref  7142  funsndifnop  7148  fmptsng  7166  fmptsnd  7167  fvsng  7178  resfunexg  7214  fveqf1o  7303  fliftel  7310  fliftel1  7311  oprabidw  7444  oprabid  7445  dfoprab2  7471  oprabv  7473  rnoprab  7518  eloprabga  7522  ot1stg  8000  ot2ndg  8001  ot3rdg  8002  fo1st  8006  fo2nd  8007  br1steqg  8008  br2ndeqg  8009  opiota  8056  eloprabi  8060  mposn  8100  fpar  8113  fsplitfpar  8115  opco1  8120  opco2  8121  frxp  8124  xporderlem  8125  fnwelem  8129  fvproj  8132  fimaproj  8133  xpord2lem  8140  xpord2pred  8143  xpord2indlem  8145  frxp3  8149  mpoxopoveq  8217  brtpos  8233  dmtpos  8236  rntpos  8237  tpostpos  8244  tfrlem11  8377  seqomlem1  8439  seqomlem3  8441  seqomlem4  8442  omeu  8572  naddcllem  8664  iiner  8789  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  10655  addpipq2  10945  addpqnq  10947  mulpipq2  10948  mulpqnq  10950  ordpipq  10951  prlem934  11042  addcnsr  11144  mulcnsr  11145  ltresr  11149  addcnsrec  11152  mulcnsrec  11153  axcnre  11173  om2uzrdg  14020  uzrdg0i  14023  uzrdgsuci  14024  hashfun  14502  wrdexb  14590  s1len  14673  s1nz  14674  s111  14683  wrdlen2i  15013  brintclab  15074  fsumcnv  15859  fprodcnv  16070  ruclem1  16319  ruclem4  16322  eucalgval2  16671  crth  16869  phimullem  16870  setsval  17259  setsdm  17262  setsfun  17263  setsfun0  17264  setsexstruct2  17267  setsres  17270  setscom  17272  strfv  17295  setsid  17299  imasaddfnlem  17614  imasaddvallem  17615  imasvscafn  17623  idfuval  17965  cofuval  17971  resfval  17981  resfval2  17982  elhoma  18121  embedsetcestrclem  18245  xpcco  18271  xpcid  18277  1stfval  18279  2ndfval  18282  prfval  18287  prf1  18288  prf2  18290  evlfval  18305  curfval  18311  curf1  18313  curfcl  18320  hofval  18340  intopsn  18746  mgm1  18750  sgrp1  18831  mnd1  18886  mnd1id  18887  degenmgm  19050  degenmgm2nfun  19052  degenmgm2  19053  grpss  19078  grp1  19170  symg2bas  19520  efgmval  19839  efgi  19846  efgi2  19852  frgpnabllem1  20000  frgpnabllem2  20001  ring1  20452  rngqiprngimfv  21501  rngqiprngimf1  21503  opsrtoslem2  22272  mat1dimelbas  22693  mat1dimbas  22694  mat1dimscm  22697  mat1dimmul  22698  mat1f1o  22700  mat1rhmelval  22702  mvmulfval  22764  m2detleib  22853  txcnp  23846  upxp  23849  uptx  23851  txdis1cn  23861  hauseqlcld  23872  txlm  23874  xkoinjcn  23913  txflf  24232  qustgplem  24347  ucnima  24506  ucnprima  24507  fmucndlem  24516  imasdsf1olem  24599  cnheiborlem  25182  ovollb2lem  25716  ovolctb  25718  ovolshftlem1  25737  ovolscalem1  25741  ovolicc1  25744  ioombl1lem3  25788  ioombl1lem4  25789  ioorval  25802  dyadval  25820  mbfimaopnlem  25883  limccnp2  26119  addsval  28227  mulsval  28374  precsexlem1  28472  precsexlem2  28473  precsexlem3  28474  om2noseqrdg  28569  noseqrdg0  28572  noseqrdgsuc  28573  brbtwn  29356  brcgr  29357  eengbas  29438  ebtwntg  29439  ecgrtg  29440  elntg  29441  structvtxval  29478  structgrssvtx  29481  structgrssiedg  29482  gropd  29488  isuhgrop  29527  uhgrunop  29532  upgrop  29551  upgr0eop  29571  upgrunop  29576  umgrunop  29578  isuspgrop  29621  isusgrop  29622  ausgrusgrb  29625  usgr0eop  29706  griedg0ssusgr  29725  uhgrspanop  29756  uhgrspan1  29763  upgrres  29766  umgrres  29767  usgrres  29768  upgrres1  29773  umgrres1  29774  usgrres1  29775  usgrexi  29901  cusgrexi  29903  cffldtocusgr  29907  cusgrres  29908  vtxdgop  29930  umgr2v2e  29985  wlkp1lem2  30132  wlkswwlksf1o  30347  wwlksnext  30361  eupth2eucrct  30697  eupthvdres  30715  konigsbergumgr  30731  numclwwlk1lem2fv  30836  numclwlk1lem1  30849  ex-br  30911  ex-fpar  30942  cnnvg  31159  cnnvs  31161  cnnvnm  31162  h2hva  31455  h2hsm  31456  h2hnm  31457  hhssva  31738  hhsssm  31739  hhssnm  31740  hhshsslem1  31748  br8d  33081  xppreima2  33124  aciunf1lem  33135  ofpreima  33138  rlocaddval  33709  rlocmulval  33710  linds2eq  33814  selvply1rhmlema  34028  selvply1rhmlem1  34030  selvply1rhmlem2  34031  smatrcl  34306  smatlem  34307  txomap  34344  qtophaus  34346  hgt750lemb  35164  bnj97  35375  bnj553  35407  bnj966  35453  bnj1442  35558  erdszelem9  35778  erdszelem10  35779  txpconn  35811  txsconnlem  35819  goel  35926  goeleq12bg  35928  gonafv  35929  gonanegoal  35931  sat1el2xp  35958  fmlaomn0  35969  gonan0  35971  goaln0  35972  gonarlem  35973  gonar  35974  goalrlem  35975  goalr  35976  fmla0disjsuc  35977  fmlasucdisj  35978  satffunlem  35980  satffunlem1lem1  35981  satffunlem2lem1  35983  satfv0fvfmla0  35992  sategoelfvb  35998  prv1n  36010  msubval  36104  mvhval  36113  msubvrs  36139  brtpid1  36300  brtpid2  36301  brtpid3  36302  br8  36335  br6  36336  br4  36337  dfdm5  36352  dfrn5  36353  elima4  36355  fv1stcnv  36356  fv2ndcnv  36357  brtxp  36457  brpprod  36462  brpprod3b  36464  brsset  36466  brtxpsd  36471  dffun10  36491  elfuns  36492  brcart  36509  brimg  36514  brapply  36515  brcup  36516  brcap  36517  lemsuccf  36518  brrestrict  36528  dfrecs2  36529  dfrdg4  36530  fvtransport  36612  brcolinear2  36638  colineardim1  36641  brsegle  36688  fvline  36724  ellines  36732  nmulprop  36770  filnetlem3  36999  bj-inftyexpitaufo  37954  bj-inftyexpitaudisj  37957  bj-inftyexpiinv  37960  bj-inftyexpidisj  37962  bj-elccinfty  37966  bj-minftyccb  37977  finxpreclem2  38144  finxp0  38145  finxp1o  38146  finxpreclem3  38147  finxpreclem4  38148  finxpreclem5  38149  finxpreclem6  38150  poimirlem9  38378  poimirlem15  38384  poimirlem17  38386  poimirlem20  38389  poimirlem24  38393  poimirlem28  38397  mblfinlem2  38407  heiborlem6  38566  heiborlem7  38567  heiborlem8  38568  grposnOLD  38632  rngosn3  38674  gidsn  38702  zrdivrng  38703  brxrn  39131  ecxrn2  39156  br1cossxrnres  39286  dvhvaddval  41963  dvhvscaval  41972  dibglbN  42039  dihglbcpreN  42173  dihmeetlem4preN  42179  dihmeetlem13N  42192  hdmapfval  42700  elcnvlem  44441  cotrintab  44454  elimaint  44489  snhesn  44626  nregmodellem  45839  projf1o  46028  dvnprodlem1  46774  dvnprodlem2  46775  sge0xp  47257  hoicvr  47376  hoicvrrex  47384  hoidmv1le  47422  hoi2toco  47435  ovnlecvr2  47438  ovolval5lem2  47481  fsetsnf1  47940  setsidel  48276  prproropf1olem3  48405  prproropf1olem4  48406  prproropreud  48409  isisubgr  48778  ushggricedg  48843  gpgusgralem  48972  gpgvtxedg0  48979  gpgvtxedg1  48980  gpg5nbgrvtx03starlem1  48984  gpg5nbgrvtx03starlem2  48985  gpg5nbgrvtx03starlem3  48986  gpg5nbgrvtx13starlem1  48987  gpg5nbgrvtx13starlem2  48988  gpg5nbgrvtx13starlem3  48989  gpg3nbgrvtx0  48992  gpg3nbgrvtx0ALT  48993  gpg3nbgrvtx1  48994  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  gpg3kgrtriex  49005  gpgprismgr4cycllem2  49012  gpgprismgr4cycllem6  49016  gpgprismgr4cycllem7  49017  gpgprismgr4cycllem10  49020  gpg5edgnedg  49046  lmod1lem2  49418  lmod1lem3  49419  lmod1zr  49423  zlmodzxznm  49427  zlmodzxzldeplem  49428  rrx2xpref1o  49648  line2x  49684  inlinecirc02plem  49716  iinxp  49759  ovsng  49786  eloprab1st2nd  49796  tposid  49811  tposidres  49812  initc  50017  rescofuf  50019  idfurcl  50024  imaf1hom  50034  oppffn  50050  oppfvalg  50052  swapfval  50188  swapf1a  50195  swapf2a  50197  swapf1  50198  swapf2  50200  fucofvalg  50244  fucofval  50245  fucofvalne  50251  fuco21  50262  fucof21  50273  prcofvalg  50302  prcofvala  50303  prcofval  50304  thincciso  50379  setc1ocofval  50420  functermceu  50436  termcfuncval  50458  fucterm  50468  0fucterm  50469  relran  50550  ranval3  50557  ranrcl4lem  50564  ranup  50568  initocmd  50595