Theorem opex 5431

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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-in 4091  df-un 4151  df-sn 4585  df-pr 4587  df-op 4835

This theorem is used by:  otex  5433  brv  5440  otth2  5451  otthg  5453  sbcop1  5457  oteqex2  5470  oteqex  5471  snopeqop  5477  propeqop  5478  propssopi  5479  euop2  5484  brsnop  5495  brtp  5496  opabidw  5497  opabid  5498  elopab  5500  rexopabb  5501  opabn0  5527  opeliunxp  5717  opeliun2xp  5718  elvvv  5726  opbrop  5748  relsnopg  5780  xpiindi  5811  raliunxp  5815  idrefALT  6106  intirr  6111  xpnz  6149  dmsnn0  6208  dmsnopg  6214  cnvcnvsn  6220  op2ndb  6228  opswap  6230  cnviin  6289  reuop  6296  dfpo2  6299  funopg  6575  dffv2  6981  fsn  7137  f1o2sn  7146  idref  7150  funsndifnop  7156  fmptsng  7174  fmptsnd  7175  fvsng  7186  resfunexg  7222  fveqf1o  7311  fliftel  7318  fliftel1  7319  oprabidw  7452  oprabid  7453  dfoprab2  7479  oprabv  7481  rnoprab  7526  eloprabga  7530  ot1stg  8016  ot2ndg  8017  ot3rdg  8018  fo1st  8022  fo2nd  8023  br1steqg  8024  br2ndeqg  8025  opiota  8071  eloprabi  8075  mposn  8117  fpar  8130  fsplitfpar  8132  opco1  8137  opco2  8138  frxp  8141  xporderlem  8142  fnwelem  8146  fvproj  8154  fimaproj  8155  xpord2lem  8162  xpord2pred  8165  xpord2indlem  8167  frxp3  8171  mpoxopoveq  8240  brtpos  8256  dmtpos  8259  rntpos  8260  tpostpos  8267  tfrlem11  8400  seqomlem1  8464  seqomlem3  8466  seqomlem4  8467  omeu  8597  naddcllem  8689  iiner  8814  xpsnen  9084  xpcomco  9090  xpassen  9094  xpmapenlem  9167  dif1en  9181  unxpdomlem1  9251  inlresf  9999  inrresf  10001  djur  10004  djuss  10005  djuun  10011  1stinl  10012  2ndinl  10013  1stinr  10014  2ndinr  10015  fseqenlem2  10108  dju1dif  10255  fpwwe  10735  addpipq2  11025  addpqnq  11027  mulpipq2  11028  mulpqnq  11030  ordpipq  11031  prlem934  11122  addcnsr  11224  mulcnsr  11225  ltresr  11229  addcnsrec  11232  mulcnsrec  11233  axcnre  11253  om2uzrdg  14103  uzrdg0i  14106  uzrdgsuci  14107  hashfun  14586  wrdexb  14674  s1len  14757  s1nz  14758  s111  14768  wrdlen2i  15099  brintclab  15160  fsumcnv  15945  fprodcnv  16156  ruclem1  16405  ruclem4  16408  eucalgval2  16762  crth  16961  phimullem  16962  setsval  17351  setsdm  17354  setsfun  17355  setsfun0  17356  setsexstruct2  17359  setsres  17362  setscom  17364  strfv  17387  setsid  17391  imasaddfnlem  17706  imasaddvallem  17707  imasvscafn  17715  idfuval  18057  cofuval  18063  resfval  18073  resfval2  18074  elhoma  18213  embedsetcestrclem  18337  xpcco  18363  xpcid  18369  1stfval  18371  2ndfval  18374  prfval  18379  prf1  18380  prf2  18382  evlfval  18397  curfval  18403  curf1  18405  curfcl  18412  hofval  18432  intopsn  18838  mgm1  18842  sgrp1  18924  mnd1  18979  mnd1id  18980  degenmgm  19143  degenmgm2nfun  19145  degenmgm2  19146  grpss  19171  grp1  19263  symg2bas  19613  efgmval  19932  efgi  19939  efgi2  19945  frgpnabllem1  20093  frgpnabllem2  20094  ring1  20547  rngqiprngimfv  21600  rngqiprngimf1  21602  opsrtoslem2  22371  mat1dimelbas  22792  mat1dimbas  22793  mat1dimscm  22796  mat1dimmul  22797  mat1f1o  22799  mat1rhmelval  22801  mvmulfval  22863  m2detleib  22952  txcnp  23945  upxp  23948  uptx  23950  txdis1cn  23960  hauseqlcld  23971  txlm  23973  xkoinjcn  24012  txflf  24331  qustgplem  24446  ucnima  24605  ucnprima  24606  fmucndlem  24615  imasdsf1olem  24698  cnheiborlem  25281  ovollb2lem  25815  ovolctb  25817  ovolshftlem1  25836  ovolscalem1  25840  ovolicc1  25843  ioombl1lem3  25887  ioombl1lem4  25888  ioorval  25901  dyadval  25919  mbfimaopnlem  25982  limccnp2  26218  addsval  28354  mulsval  28501  precsexlem1  28599  precsexlem2  28600  precsexlem3  28601  om2noseqrdg  28696  noseqrdg0  28699  noseqrdgsuc  28700  brbtwn  29483  brcgr  29484  eengbas  29565  ebtwntg  29566  ecgrtg  29567  elntg  29568  structvtxval  29605  structgrssvtx  29608  structgrssiedg  29609  gropd  29615  isuhgrop  29654  uhgrunop  29659  upgrop  29678  upgr0eop  29698  upgrunop  29703  umgrunop  29705  isuspgrop  29748  isusgrop  29749  ausgrusgrb  29752  usgr0eop  29833  griedg0ssusgr  29852  uhgrspanop  29883  uhgrspan1  29890  upgrres  29893  umgrres  29894  usgrres  29895  upgrres1  29900  umgrres1  29901  usgrres1  29902  usgrexi  30028  cusgrexi  30030  cffldtocusgr  30034  cusgrres  30035  vtxdgop  30057  umgr2v2e  30112  wlkp1lem2  30259  wlkswwlksf1o  30474  wwlksnext  30488  eupth2eucrct  30824  eupthvdres  30842  konigsbergumgr  30858  numclwwlk1lem2fv  30963  numclwlk1lem1  30976  ex-br  31038  ex-fpar  31069  cnnvg  31286  cnnvs  31288  cnnvnm  31289  h2hva  31582  h2hsm  31583  h2hnm  31584  hhssva  31865  hhsssm  31866  hhssnm  31867  hhshsslem1  31875  br8d  33250  xppreima2  33293  aciunf1lem  33304  ofpreima  33307  rlocaddval  33877  rlocmulval  33878  linds2eq  33983  selvply1rhmlema  34197  selvply1rhmlem1  34199  selvply1rhmlem2  34200  smatrcl  34475  smatlem  34476  txomap  34513  qtophaus  34515  hgt750lemb  35332  bnj97  35543  bnj553  35575  bnj966  35621  bnj1442  35726  j0ltalephlem  35947  erdszelem9  36051  erdszelem10  36052  txpconn  36084  txsconnlem  36092  goel  36199  goeleq12bg  36201  gonafv  36202  gonanegoal  36204  sat1el2xp  36231  fmlaomn0  36242  gonan0  36244  goaln0  36245  gonarlem  36246  gonar  36247  goalrlem  36248  goalr  36249  fmla0disjsuc  36250  fmlasucdisj  36251  satffunlem  36253  satffunlem1lem1  36254  satffunlem2lem1  36256  satfv0fvfmla0  36265  sategoelfvb  36271  prv1n  36283  msubval  36377  mvhval  36386  msubvrs  36412  brtpid1  36579  brtpid2  36580  brtpid3  36581  br8  36614  br6  36615  br4  36616  dfdm5  36630  dfrn5  36631  elima4  36633  fv1stcnv  36634  fv2ndcnv  36635  brtxp  36735  brpprod  36740  brpprod3b  36742  brsset  36744  brtxpsd  36749  dffun10  36769  elfuns  36770  brcart  36787  brimg  36792  brapply  36793  brcup  36794  brcap  36795  lemsuccf  36796  brrestrict  36806  dfrecs2  36807  dfrdg4  36808  fvtransport  36890  brcolinear2  36916  colineardim1  36919  brsegle  36966  fvline  37002  ellines  37010  nmulprop  37032  filnetlem3  37261  bj-inftyexpitaufo  38217  bj-inftyexpitaudisj  38220  bj-inftyexpiinv  38223  bj-inftyexpidisj  38225  bj-elccinfty  38229  bj-minftyccb  38240  finxpreclem2  38407  finxp0  38408  finxp1o  38409  finxpreclem3  38410  finxpreclem4  38411  finxpreclem5  38412  finxpreclem6  38413  poimirlem9  38641  poimirlem15  38647  poimirlem17  38649  poimirlem20  38652  poimirlem24  38656  poimirlem28  38660  mblfinlem2  38670  heiborlem6  38844  heiborlem7  38845  heiborlem8  38846  grposnOLD  38910  rngosn3  38952  gidsn  38980  zrdivrng  38981  brxrn  39409  ecxrn2  39434  br1cossxrnres  39564  dvhvaddval  42241  dvhvscaval  42250  dibglbN  42317  dihglbcpreN  42451  dihmeetlem4preN  42457  dihmeetlem13N  42470  hdmapfval  42978  elcnvlem  44695  cotrintab  44708  elimaint  44743  snhesn  44880  nregmodellem  46100  projf1o  46305  dvnprodlem1  47050  dvnprodlem2  47051  sge0xp  47533  hoicvr  47652  hoicvrrex  47660  hoidmv1le  47698  hoi2toco  47711  ovnlecvr2  47714  ovolval5lem2  47757  fsetsnf1  48216  setsidel  48552  prproropf1olem3  48681  prproropf1olem4  48682  prproropreud  48685  isisubgr  49054  ushggricedg  49119  gpgusgralem  49248  gpgvtxedg0  49255  gpgvtxedg1  49256  gpg5nbgrvtx03starlem1  49260  gpg5nbgrvtx03starlem2  49261  gpg5nbgrvtx03starlem3  49262  gpg5nbgrvtx13starlem1  49263  gpg5nbgrvtx13starlem2  49264  gpg5nbgrvtx13starlem3  49265  gpg3nbgrvtx0  49268  gpg3nbgrvtx0ALT  49269  gpg3nbgrvtx1  49270  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  gpg3kgrtriex  49281  gpgprismgr4cycllem2  49288  gpgprismgr4cycllem6  49292  gpgprismgr4cycllem7  49293  gpgprismgr4cycllem10  49296  gpg5edgnedg  49322  lmod1lem2  49694  lmod1lem3  49695  lmod1zr  49699  zlmodzxznm  49703  zlmodzxzldeplem  49704  iinxp  50036  ovsng  50063  eloprab1st2nd  50073  tposid  50092  tposidres  50093  initc  50300  rescofuf  50302  idfurcl  50308  imaf1hom  50318  oppffn  50334  oppfvalg  50336  swapfval  50478  swapf1a  50485  swapf2a  50487  swapf1  50488  swapf2  50490  fucofvalg  50534  fucofval  50535  fucofvalne  50541  fuco21  50552  fucof21  50563  prcofvalg  50605  prcofvala  50606  prcofval  50607  thincciso  50682  setc1ocofval  50723  functermceu  50739  termcfuncval  50761  fucterm  50774  0fucterm  50775  relran  50901  ranval3  50908  ranrcl4lem  50915  ranup  50919  initocmd  50946