Theorem opex 5428

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 5253. (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 4586	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1150	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5392	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5279	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2857	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1097   ∈ wcel 2141  {cab 2739  Vcvv 3453  {csn 4579  {cpr 4581  ⟨cop 4585

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5243  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-un 3907  df-in 3909  df-ss 3919  df-sn 4580  df-pr 4582  df-op 4586

This theorem is referenced by:  otex  5430  brv  5437  otth2  5448  otthg  5450  sbcop1  5453  oteqex2  5465  oteqex  5466  snopeqop  5472  propeqop  5473  propssopi  5474  euop2  5478  brsnop  5489  brtp  5490  opabidw  5491  opabid  5492  elopab  5494  rexopabb  5495  opabn0  5520  opeliunxp  5710  opeliun2xp  5711  elvvv  5719  opbrop  5741  relsnopg  5772  xpiindi  5803  raliunxp  5807  idrefALT  6095  intirr  6100  xpnz  6139  dmsnn0  6188  dmsnopg  6194  cnvcnvsn  6200  op2ndb  6208  opswap  6210  cnviin  6267  reuop  6274  dfpo2  6277  funopg  6549  dffv2  6956  fsn  7111  f1o2sn  7118  idref  7122  funsndifnop  7128  fmptsng  7146  fmptsnd  7147  fvsng  7158  resfunexg  7193  fveqf1o  7280  fliftel  7287  fliftel1  7288  oprabidw  7421  oprabid  7422  dfoprab2  7448  oprabv  7450  rnoprab  7495  eloprabga  7499  ot1stg  7978  ot2ndg  7979  ot3rdg  7980  fo1st  7984  fo2nd  7985  br1steqg  7986  br2ndeqg  7987  opiota  8034  eloprabi  8038  mposn  8075  fpar  8088  fsplitfpar  8090  opco1  8095  opco2  8096  frxp  8099  xporderlem  8100  fnwelem  8104  fvproj  8107  fimaproj  8108  xpord2lem  8115  xpord2pred  8118  xpord2indlem  8120  frxp3  8124  mpoxopoveq  8192  brtpos  8208  dmtpos  8211  rntpos  8212  tpostpos  8219  tfrlem11  8352  seqomlem1  8414  seqomlem3  8416  seqomlem4  8417  omeu  8547  naddcllem  8639  iiner  8764  xpsnen  9026  xpcomco  9032  xpassen  9036  xpmapenlem  9109  dif1en  9123  unxpdomlem1  9193  inlresf  9865  inrresf  9867  djur  9870  djuss  9871  djuun  9877  1stinl  9878  2ndinl  9879  1stinr  9880  2ndinr  9881  fseqenlem2  9974  dju1dif  10122  fpwwe  10597  addpipq2  10887  addpqnq  10889  mulpipq2  10890  mulpqnq  10892  ordpipq  10893  prlem934  10984  addcnsr  11086  mulcnsr  11087  ltresr  11091  addcnsrec  11094  mulcnsrec  11095  axcnre  11115  om2uzrdg  13962  uzrdg0i  13965  uzrdgsuci  13966  hashfun  14443  wrdexb  14531  s1len  14613  s1nz  14614  s111  14622  wrdlen2i  14948  brintclab  15007  fsumcnv  15790  fprodcnv  16003  ruclem1  16253  ruclem4  16256  eucalgval2  16605  crth  16803  phimullem  16804  setsval  17193  setsdm  17196  setsfun  17197  setsfun0  17198  setsexstruct2  17201  setsres  17204  setscom  17206  strfv  17229  setsid  17233  imasaddfnlem  17548  imasaddvallem  17549  imasvscafn  17557  idfuval  17899  cofuval  17905  resfval  17915  resfval2  17916  elhoma  18055  embedsetcestrclem  18179  xpcco  18205  xpcid  18211  1stfval  18213  2ndfval  18216  prfval  18221  prf1  18222  prf2  18224  evlfval  18239  curfval  18245  curf1  18247  curfcl  18254  hofval  18274  intopsn  18678  mgm1  18682  sgrp1  18753  mnd1  18803  mnd1id  18804  grpss  18986  grp1  19079  symg2bas  19423  efgmval  19742  efgi  19749  efgi2  19755  frgpnabllem1  19903  frgpnabllem2  19904  ring1  20346  rngqiprngimfv  21355  rngqiprngimf1  21357  opsrtoslem2  22096  mat1dimelbas  22518  mat1dimbas  22519  mat1dimscm  22522  mat1dimmul  22523  mat1f1o  22525  mat1rhmelval  22527  mvmulfval  22589  m2detleib  22678  txcnp  23667  upxp  23670  uptx  23672  txdis1cn  23682  hauseqlcld  23693  txlm  23695  xkoinjcn  23734  txflf  24053  qustgplem  24168  ucnima  24327  ucnprima  24328  fmucndlem  24337  imasdsf1olem  24420  cnheiborlem  25003  ovollb2lem  25537  ovolctb  25539  ovolshftlem1  25558  ovolscalem1  25562  ovolicc1  25565  ioombl1lem3  25609  ioombl1lem4  25610  ioorval  25623  dyadval  25641  mbfimaopnlem  25704  limccnp2  25941  addsval  28042  mulsval  28189  precsexlem1  28287  precsexlem2  28288  precsexlem3  28289  om2noseqrdg  28384  noseqrdg0  28387  noseqrdgsuc  28388  brbtwn  29056  brcgr  29057  eengbas  29138  ebtwntg  29139  ecgrtg  29140  elntg  29141  structvtxval  29178  structgrssvtx  29181  structgrssiedg  29182  gropd  29188  isuhgrop  29227  uhgrunop  29232  upgrop  29251  upgr0eop  29271  upgrunop  29276  umgrunop  29278  isuspgrop  29318  isusgrop  29319  ausgrusgrb  29322  usgr0eop  29403  griedg0ssusgr  29422  uhgrspanop  29453  uhgrspan1  29460  upgrres  29463  umgrres  29464  usgrres  29465  upgrres1  29470  umgrres1  29471  usgrres1  29472  usgrexi  29598  cusgrexi  29600  cffldtocusgr  29604  cusgrres  29605  vtxdgop  29627  umgr2v2e  29682  wlkp1lem2  29829  wlkswwlksf1o  30035  wwlksnext  30049  eupth2eucrct  30375  eupthvdres  30393  konigsbergumgr  30409  numclwwlk1lem2fv  30514  numclwlk1lem1  30527  ex-br  30589  ex-fpar  30620  cnnvg  30837  cnnvs  30839  cnnvnm  30840  h2hva  31133  h2hsm  31134  h2hnm  31135  hhssva  31416  hhsssm  31417  hhssnm  31418  hhshsslem1  31426  br8d  32770  xppreima2  32813  aciunf1lem  32824  ofpreima  32827  rlocaddval  33410  rlocmulval  33411  linds2eq  33527  selvply1rhmlema  33775  selvply1rhmlem1  33777  selvply1rhmlem2  33778  smatrcl  34053  smatlem  34054  txomap  34091  qtophaus  34093  hgt750lemb  34910  bnj97  35121  bnj553  35153  bnj966  35199  bnj1442  35304  erdszelem9  35509  erdszelem10  35510  txpconn  35542  txsconnlem  35550  goel  35657  goeleq12bg  35659  gonafv  35660  gonanegoal  35662  sat1el2xp  35689  fmlaomn0  35700  gonan0  35702  goaln0  35703  gonarlem  35704  gonar  35705  goalrlem  35706  goalr  35707  fmla0disjsuc  35708  fmlasucdisj  35709  satffunlem  35711  satffunlem1lem1  35712  satffunlem2lem1  35714  satfv0fvfmla0  35723  sategoelfvb  35729  prv1n  35741  msubval  35835  mvhval  35844  msubvrs  35870  brtpid1  36031  brtpid2  36032  brtpid3  36033  br8  36066  br6  36067  br4  36068  dfdm5  36083  dfrn5  36084  elima4  36086  fv1stcnv  36087  fv2ndcnv  36088  brtxp  36188  brpprod  36193  brpprod3b  36195  brsset  36197  brtxpsd  36202  dffun10  36222  elfuns  36223  brcart  36240  brimg  36245  brapply  36246  brcup  36247  brcap  36248  lemsuccf  36249  brrestrict  36259  dfrecs2  36260  dfrdg4  36261  fvtransport  36342  brcolinear2  36368  colineardim1  36371  brsegle  36418  fvline  36454  ellines  36462  nmulprop  36500  filnetlem3  36700  bj-inftyexpitaufo  37654  bj-inftyexpitaudisj  37657  bj-inftyexpiinv  37660  bj-inftyexpidisj  37662  bj-elccinfty  37666  bj-minftyccb  37677  finxpreclem2  37844  finxp0  37845  finxp1o  37846  finxpreclem3  37847  finxpreclem4  37848  finxpreclem5  37849  finxpreclem6  37850  poimirlem9  38088  poimirlem15  38094  poimirlem17  38096  poimirlem20  38099  poimirlem24  38103  poimirlem28  38107  mblfinlem2  38117  heiborlem6  38275  heiborlem7  38276  heiborlem8  38277  grposnOLD  38341  rngosn3  38383  gidsn  38411  zrdivrng  38412  brxrn  38842  ecxrn2  38867  br1cossxrnres  38997  dvhvaddval  41674  dvhvscaval  41683  dibglbN  41750  dihglbcpreN  41884  dihmeetlem4preN  41890  dihmeetlem13N  41903  hdmapfval  42411  elcnvlem  44137  cotrintab  44150  elimaint  44185  snhesn  44322  nregmodellem  45552  projf1o  45734  dvnprodlem1  46480  dvnprodlem2  46481  sge0xp  46963  hoicvr  47082  hoicvrrex  47090  hoidmv1le  47128  hoi2toco  47141  ovnlecvr2  47144  ovolval5lem2  47187  fsetsnf1  47606  setsidel  47942  prproropf1olem3  48071  prproropf1olem4  48072  prproropreud  48075  isisubgr  48444  ushggricedg  48509  gpgusgralem  48638  gpgvtxedg0  48645  gpgvtxedg1  48646  gpg5nbgrvtx03starlem1  48650  gpg5nbgrvtx03starlem2  48651  gpg5nbgrvtx03starlem3  48652  gpg5nbgrvtx13starlem1  48653  gpg5nbgrvtx13starlem2  48654  gpg5nbgrvtx13starlem3  48655  gpg3nbgrvtx0  48658  gpg3nbgrvtx0ALT  48659  gpg3nbgrvtx1  48660  gpg5nbgrvtx03star  48662  gpg5nbgr3star  48663  gpg3kgrtriex  48671  gpgprismgr4cycllem2  48678  gpgprismgr4cycllem6  48682  gpgprismgr4cycllem7  48683  gpgprismgr4cycllem10  48686  gpg5edgnedg  48712  lmod1lem2  49070  lmod1lem3  49071  lmod1zr  49075  zlmodzxznm  49079  zlmodzxzldeplem  49080  rrx2xpref1o  49300  line2x  49336  inlinecirc02plem  49368  iinxp  49412  ovsng  49439  eloprab1st2nd  49449  tposid  49466  tposidres  49467  initc  49672  rescofuf  49674  idfurcl  49679  imaf1hom  49689  oppffn  49705  oppfvalg  49707  swapfval  49843  swapf1a  49850  swapf2a  49852  swapf1  49853  swapf2  49855  fucofvalg  49899  fucofval  49900  fucofvalne  49906  fuco21  49917  fucof21  49928  prcofvalg  49957  prcofvala  49958  prcofval  49959  thincciso  50034  setc1ocofval  50075  functermceu  50091  termcfuncval  50113  fucterm  50123  0fucterm  50124  relran  50205  ranval3  50212  ranrcl4lem  50219  ranup  50223  initocmd  50250