Theorem opex 5437

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 5264. (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 4839	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1156	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5401	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5293	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2860	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

This proof depends on syntax axioms:   ∧ w3a 1103   ∈ wcel 2147  {cab 2741  Vcvv 3454  {csn 4588  {cpr 4590  ⟨cop 4838

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5253  ax-pr 5396

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-in 4094  df-un 4154  df-sn 4589  df-pr 4591  df-op 4839

This theorem is used by:  otex  5439  brv  5446  otth2  5457  otthg  5459  sbcop1  5463  oteqex2  5476  oteqex  5477  snopeqop  5483  propeqop  5484  propssopi  5485  euop2  5490  brsnop  5501  brtp  5502  opabidw  5503  opabid  5504  elopab  5506  rexopabb  5507  opabn0  5533  opeliunxp  5723  opeliun2xp  5724  elvvv  5733  opbrop  5755  relsnopg  5788  xpiindi  5820  raliunxp  5824  idrefALT  6123  intirr  6128  xpnz  6166  dmsnn0  6225  dmsnopg  6231  cnvcnvsn  6237  op2ndb  6245  opswap  6247  cnviin  6311  reuop  6320  dfpo2  6323  funopg  6600  dffv2  7009  fsn  7166  f1o2sn  7175  idref  7179  funsndifnop  7185  fmptsng  7202  fmptsnd  7203  fvsng  7214  resfunexg  7250  fveqf1o  7339  fliftel  7346  fliftel1  7347  oprabidw  7480  oprabid  7481  dfoprab2  7507  oprabv  7509  rnoprab  7554  eloprabga  7558  ot1stg  8047  ot2ndg  8048  ot3rdg  8049  fo1st  8053  fo2nd  8054  br1steqg  8055  br2ndeqg  8056  opiota  8103  eloprabi  8107  mposn  8149  fpar  8162  fsplitfpar  8164  opco1  8169  opco2  8170  frxp  8173  xporderlem  8174  fnwelem  8178  fvproj  8186  fimaproj  8187  xpord2lem  8194  xpord2pred  8197  xpord2indlem  8199  frxp3  8203  mpoxopoveq  8272  brtpos  8288  dmtpos  8291  rntpos  8292  tpostpos  8299  tfrlem11  8432  seqomlem1  8496  seqomlem3  8498  seqomlem4  8499  omeu  8629  naddcllem  8721  iiner  8846  xpsnen  9116  xpcomco  9122  xpassen  9126  xpmapenlem  9199  dif1en  9213  unxpdomlem1  9283  inlresf  10030  inrresf  10032  djur  10035  djuss  10036  djuun  10042  1stinl  10043  2ndinl  10044  1stinr  10045  2ndinr  10046  fseqenlem2  10141  dju1dif  10288  fpwwe  10768  addpipq2  11058  addpqnq  11060  mulpipq2  11061  mulpqnq  11063  ordpipq  11064  prlem934  11155  addcnsr  11257  mulcnsr  11258  ltresr  11262  addcnsrec  11265  mulcnsrec  11266  axcnre  11286  om2uzrdg  14137  uzrdg0i  14140  uzrdgsuci  14141  hashfun  14621  wrdexb  14709  s1len  14792  s1nz  14793  s111  14803  wrdlen2i  15134  brintclab  15195  fsumcnv  15980  fprodcnv  16191  ruclem1  16440  ruclem4  16443  eucalgval2  16797  crth  16996  phimullem  16997  setsval  17386  setsdm  17389  setsfun  17390  setsfun0  17391  setsexstruct2  17394  setsres  17397  setscom  17399  strfv  17422  setsid  17426  imasaddfnlem  17741  imasaddvallem  17742  imasvscafn  17750  idfuval  18092  cofuval  18098  resfval  18108  resfval2  18109  elhoma  18248  embedsetcestrclem  18372  xpcco  18398  xpcid  18404  1stfval  18406  2ndfval  18409  prfval  18414  prf1  18415  prf2  18417  evlfval  18432  curfval  18438  curf1  18440  curfcl  18447  hofval  18467  intopsn  18873  mgm1  18877  sgrp1  18959  mnd1  19014  mnd1id  19015  degenmgm  19178  degenmgm2nfun  19180  degenmgm2  19181  grpss  19206  grp1  19298  symg2bas  19649  efgmval  19968  efgi  19975  efgi2  19981  frgpnabllem1  20129  frgpnabllem2  20130  ring1  20583  rngqiprngimfv  21636  rngqiprngimf1  21638  opsrtoslem2  22409  mat1dimelbas  22830  mat1dimbas  22831  mat1dimscm  22834  mat1dimmul  22835  mat1f1o  22837  mat1rhmelval  22839  mvmulfval  22901  m2detleib  22990  txcnp  23983  upxp  23986  uptx  23988  txdis1cn  23998  hauseqlcld  24009  txlm  24011  xkoinjcn  24050  txflf  24369  qustgplem  24484  ucnima  24643  ucnprima  24644  fmucndlem  24653  imasdsf1olem  24736  cnheiborlem  25319  ovollb2lem  25853  ovolctb  25855  ovolshftlem1  25874  ovolscalem1  25878  ovolicc1  25881  ioombl1lem3  25925  ioombl1lem4  25926  ioorval  25939  dyadval  25957  mbfimaopnlem  26020  limccnp2  26256  addsval  28394  mulsval  28541  precsexlem1  28639  precsexlem2  28640  precsexlem3  28641  om2noseqrdg  28736  noseqrdg0  28739  noseqrdgsuc  28740  brbtwn  29523  brcgr  29524  eengbas  29605  ebtwntg  29606  ecgrtg  29607  elntg  29608  structvtxval  29645  structgrssvtx  29648  structgrssiedg  29649  gropd  29655  isuhgrop  29694  uhgrunop  29699  upgrop  29718  upgr0eop  29738  upgrunop  29743  umgrunop  29745  isuspgrop  29788  isusgrop  29789  ausgrusgrb  29792  usgr0eop  29873  griedg0ssusgr  29892  uhgrspanop  29923  uhgrspan1  29930  upgrres  29933  umgrres  29934  usgrres  29935  upgrres1  29940  umgrres1  29941  usgrres1  29942  usgrexi  30068  cusgrexi  30070  cffldtocusgr  30074  cusgrres  30075  vtxdgop  30097  umgr2v2e  30152  wlkp1lem2  30299  wlkswwlksf1o  30514  wwlksnext  30528  eupth2eucrct  30864  eupthvdres  30882  konigsbergumgr  30898  numclwwlk1lem2fv  31003  numclwlk1lem1  31016  ex-br  31078  ex-fpar  31109  cnnvg  31326  cnnvs  31328  cnnvnm  31329  h2hva  31622  h2hsm  31623  h2hnm  31624  hhssva  31905  hhsssm  31906  hhssnm  31907  hhshsslem1  31915  br8d  33290  xppreima2  33333  aciunf1lem  33344  ofpreima  33347  rlocaddval  33919  rlocmulval  33920  linds2eq  34033  selvply1rhmlema  34254  selvply1rhmlem1  34256  selvply1rhmlem2  34257  smatrcl  34532  smatlem  34533  txomap  34570  qtophaus  34572  hgt750lemb  35389  bnj97  35600  bnj553  35632  bnj966  35678  bnj1442  35783  omeueq  35830  j0ltalephlem  36041  dfj2  36043  erdszelem9  36165  erdszelem10  36166  txpconn  36198  txsconnlem  36206  goel  36313  goeleq12bg  36315  gonafv  36316  gonanegoal  36318  sat1el2xp  36345  fmlaomn0  36356  gonan0  36358  goaln0  36359  gonarlem  36360  gonar  36361  goalrlem  36362  goalr  36363  fmla0disjsuc  36364  fmlasucdisj  36365  satffunlem  36367  satffunlem1lem1  36368  satffunlem2lem1  36370  satfv0fvfmla0  36379  sategoelfvb  36385  prv1n  36397  msubval  36491  mvhval  36500  msubvrs  36526  brtpid1  36694  brtpid2  36695  brtpid3  36696  br8  36729  br6  36730  br4  36731  dfdm5  36745  dfrn5  36746  elima4  36748  fv1stcnv  36749  fv2ndcnv  36750  brtxp  36850  brpprod  36855  brpprod3b  36857  brsset  36859  brtxpsd  36864  dffun10  36884  elfuns  36885  brcart  36902  brimg  36907  brapply  36908  brcup  36909  brcap  36910  lemsuccf  36911  brrestrict  36921  dfrecs2  36922  dfrdg4  36923  fvtransport  37005  brcolinear2  37031  colineardim1  37034  brsegle  37081  fvline  37117  ellines  37125  nmulprop  37147  filnetlem3  37376  bj-inftyexpitaufo  38384  bj-inftyexpitaudisj  38387  bj-inftyexpiinv  38390  bj-inftyexpidisj  38392  bj-elccinfty  38396  bj-minftyccb  38407  finxpreclem2  38574  finxp0  38575  finxp1o  38576  finxpreclem3  38577  finxpreclem4  38578  finxpreclem5  38579  finxpreclem6  38580  poimirlem9  38808  poimirlem15  38814  poimirlem17  38816  poimirlem20  38819  poimirlem24  38823  poimirlem28  38827  mblfinlem2  38837  heiborlem6  39009  heiborlem7  39010  heiborlem8  39011  grposnOLD  39075  rngosn3  39117  gidsn  39145  zrdivrng  39146  brxrn  39574  ecxrn2  39599  br1cossxrnres  39729  dvhvaddval  42406  dvhvscaval  42415  dibglbN  42482  dihglbcpreN  42616  dihmeetlem4preN  42622  dihmeetlem13N  42635  hdmapfval  43143  elcnvlem  44856  cotrintab  44869  elimaint  44904  snhesn  45041  nregmodellem  46264  projf1o  46478  dvnprodlem1  47223  dvnprodlem2  47224  sge0xp  47706  hoicvr  47825  hoicvrrex  47833  hoidmv1le  47871  hoi2toco  47884  ovnlecvr2  47887  ovolval5lem2  47930  fsetsnf1  48389  setsidel  48725  prproropf1olem3  48854  prproropf1olem4  48855  prproropreud  48858  isisubgr  49227  ushggricedg  49292  gpgusgralem  49421  gpgvtxedg0  49428  gpgvtxedg1  49429  gpg5nbgrvtx03starlem1  49433  gpg5nbgrvtx03starlem2  49434  gpg5nbgrvtx03starlem3  49435  gpg5nbgrvtx13starlem1  49436  gpg5nbgrvtx13starlem2  49437  gpg5nbgrvtx13starlem3  49438  gpg3nbgrvtx0  49441  gpg3nbgrvtx0ALT  49442  gpg3nbgrvtx1  49443  gpg5nbgrvtx03star  49445  gpg5nbgr3star  49446  gpg3kgrtriex  49454  gpgprismgr4cycllem2  49461  gpgprismgr4cycllem6  49465  gpgprismgr4cycllem7  49466  gpgprismgr4cycllem10  49469  gpg5edgnedg  49495  lmod1lem2  49925  lmod1lem3  49926  lmod1zr  49930  zlmodzxznm  49934  zlmodzxzldeplem  49935  iinxp  50267  ovsng  50294  eloprab1st2nd  50304  tposid  50323  tposidres  50324  initc  50531  rescofuf  50533  idfurcl  50539  imaf1hom  50549  oppffn  50565  oppfvalg  50567  swapfval  50709  swapf1a  50716  swapf2a  50718  swapf1  50719  swapf2  50721  fucofvalg  50765  fucofval  50766  fucofvalne  50772  fuco21  50783  fucof21  50794  prcofvalg  50836  prcofvala  50837  prcofval  50838  thincciso  50913  setc1ocofval  50954  functermceu  50970  termcfuncval  50992  fucterm  51005  0fucterm  51006  relran  51132  ranval3  51139  ranrcl4lem  51146  ranup  51150  initocmd  51177