Theorem opex 5447

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 5270. (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 4597	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1156	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5411	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5298	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2859	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1103   ∈ wcel 2143  {cab 2741  Vcvv 3455  {csn 4590  {cpr 4592  ⟨cop 4596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-un 3911  df-in 3913  df-ss 3923  df-sn 4591  df-pr 4593  df-op 4597

This theorem is referenced by:  otex  5449  brv  5456  otth2  5467  otthg  5469  sbcop1  5472  oteqex2  5484  oteqex  5485  snopeqop  5491  propeqop  5492  propssopi  5493  euop2  5497  brsnop  5508  brtp  5509  opabidw  5510  opabid  5511  elopab  5513  rexopabb  5514  opabn0  5540  opeliunxp  5730  opeliun2xp  5731  elvvv  5739  opbrop  5761  relsnopg  5792  xpiindi  5823  raliunxp  5827  idrefALT  6115  intirr  6120  xpnz  6158  dmsnn0  6210  dmsnopg  6216  cnvcnvsn  6222  op2ndb  6230  opswap  6232  cnviin  6289  reuop  6296  dfpo2  6299  funopg  6572  dffv2  6978  fsn  7133  f1o2sn  7140  idref  7144  funsndifnop  7150  fmptsng  7168  fmptsnd  7169  fvsng  7180  resfunexg  7215  fveqf1o  7302  fliftel  7309  fliftel1  7310  oprabidw  7443  oprabid  7444  dfoprab2  7470  oprabv  7472  rnoprab  7517  eloprabga  7521  ot1stg  8001  ot2ndg  8002  ot3rdg  8003  fo1st  8007  fo2nd  8008  br1steqg  8009  br2ndeqg  8010  opiota  8057  eloprabi  8061  mposn  8099  fpar  8112  fsplitfpar  8114  opco1  8119  opco2  8120  frxp  8123  xporderlem  8124  fnwelem  8128  fvproj  8131  fimaproj  8132  xpord2lem  8139  xpord2pred  8142  xpord2indlem  8144  frxp3  8148  mpoxopoveq  8216  brtpos  8232  dmtpos  8235  rntpos  8236  tpostpos  8243  tfrlem11  8376  seqomlem1  8438  seqomlem3  8440  seqomlem4  8441  omeu  8571  naddcllem  8663  iiner  8788  xpsnen  9050  xpcomco  9056  xpassen  9060  xpmapenlem  9133  dif1en  9147  unxpdomlem1  9217  inlresf  9901  inrresf  9903  djur  9906  djuss  9907  djuun  9913  1stinl  9914  2ndinl  9915  1stinr  9916  2ndinr  9917  fseqenlem2  10010  dju1dif  10157  fpwwe  10632  addpipq2  10922  addpqnq  10924  mulpipq2  10925  mulpqnq  10927  ordpipq  10928  prlem934  11019  addcnsr  11121  mulcnsr  11122  ltresr  11126  addcnsrec  11129  mulcnsrec  11130  axcnre  11150  om2uzrdg  13994  uzrdg0i  13997  uzrdgsuci  13998  hashfun  14476  wrdexb  14564  s1len  14646  s1nz  14647  s111  14655  wrdlen2i  14981  brintclab  15040  fsumcnv  15826  fprodcnv  16039  ruclem1  16288  ruclem4  16291  eucalgval2  16640  crth  16838  phimullem  16839  setsval  17228  setsdm  17231  setsfun  17232  setsfun0  17233  setsexstruct2  17236  setsres  17239  setscom  17241  strfv  17264  setsid  17268  imasaddfnlem  17583  imasaddvallem  17584  imasvscafn  17592  idfuval  17934  cofuval  17940  resfval  17950  resfval2  17951  elhoma  18090  embedsetcestrclem  18214  xpcco  18240  xpcid  18246  1stfval  18248  2ndfval  18251  prfval  18256  prf1  18257  prf2  18259  evlfval  18274  curfval  18280  curf1  18282  curfcl  18289  hofval  18309  intopsn  18713  mgm1  18717  sgrp1  18788  mnd1  18838  mnd1id  18839  grpss  19022  grp1  19114  symg2bas  19464  efgmval  19783  efgi  19790  efgi2  19796  frgpnabllem1  19944  frgpnabllem2  19945  ring1  20394  rngqiprngimfv  21419  rngqiprngimf1  21421  opsrtoslem2  22188  mat1dimelbas  22609  mat1dimbas  22610  mat1dimscm  22613  mat1dimmul  22614  mat1f1o  22616  mat1rhmelval  22618  mvmulfval  22680  m2detleib  22769  txcnp  23758  upxp  23761  uptx  23763  txdis1cn  23773  hauseqlcld  23784  txlm  23786  xkoinjcn  23825  txflf  24144  qustgplem  24259  ucnima  24418  ucnprima  24419  fmucndlem  24428  imasdsf1olem  24511  cnheiborlem  25094  ovollb2lem  25628  ovolctb  25630  ovolshftlem1  25649  ovolscalem1  25653  ovolicc1  25656  ioombl1lem3  25700  ioombl1lem4  25701  ioorval  25714  dyadval  25732  mbfimaopnlem  25795  limccnp2  26032  addsval  28136  mulsval  28283  precsexlem1  28381  precsexlem2  28382  precsexlem3  28383  om2noseqrdg  28478  noseqrdg0  28481  noseqrdgsuc  28482  brbtwn  29230  brcgr  29231  eengbas  29312  ebtwntg  29313  ecgrtg  29314  elntg  29315  structvtxval  29352  structgrssvtx  29355  structgrssiedg  29356  gropd  29362  isuhgrop  29401  uhgrunop  29406  upgrop  29425  upgr0eop  29445  upgrunop  29450  umgrunop  29452  isuspgrop  29492  isusgrop  29493  ausgrusgrb  29496  usgr0eop  29577  griedg0ssusgr  29596  uhgrspanop  29627  uhgrspan1  29634  upgrres  29637  umgrres  29638  usgrres  29639  upgrres1  29644  umgrres1  29645  usgrres1  29646  usgrexi  29772  cusgrexi  29774  cffldtocusgr  29778  cusgrres  29779  vtxdgop  29801  umgr2v2e  29856  wlkp1lem2  30003  wlkswwlksf1o  30209  wwlksnext  30223  eupth2eucrct  30549  eupthvdres  30567  konigsbergumgr  30583  numclwwlk1lem2fv  30688  numclwlk1lem1  30701  ex-br  30763  ex-fpar  30794  cnnvg  31011  cnnvs  31013  cnnvnm  31014  h2hva  31307  h2hsm  31308  h2hnm  31309  hhssva  31590  hhsssm  31591  hhssnm  31592  hhshsslem1  31600  br8d  32934  xppreima2  32977  aciunf1lem  32988  ofpreima  32991  rlocaddval  33570  rlocmulval  33571  linds2eq  33675  selvply1rhmlema  33889  selvply1rhmlem1  33891  selvply1rhmlem2  33892  smatrcl  34167  smatlem  34168  txomap  34205  qtophaus  34207  hgt750lemb  35024  bnj97  35235  bnj553  35267  bnj966  35313  bnj1442  35418  erdszelem9  35672  erdszelem10  35673  txpconn  35705  txsconnlem  35713  goel  35820  goeleq12bg  35822  gonafv  35823  gonanegoal  35825  sat1el2xp  35852  fmlaomn0  35863  gonan0  35865  goaln0  35866  gonarlem  35867  gonar  35868  goalrlem  35869  goalr  35870  fmla0disjsuc  35871  fmlasucdisj  35872  satffunlem  35874  satffunlem1lem1  35875  satffunlem2lem1  35877  satfv0fvfmla0  35886  sategoelfvb  35892  prv1n  35904  msubval  35998  mvhval  36007  msubvrs  36033  brtpid1  36194  brtpid2  36195  brtpid3  36196  br8  36229  br6  36230  br4  36231  dfdm5  36246  dfrn5  36247  elima4  36249  fv1stcnv  36250  fv2ndcnv  36251  brtxp  36351  brpprod  36356  brpprod3b  36358  brsset  36360  brtxpsd  36365  dffun10  36385  elfuns  36386  brcart  36403  brimg  36408  brapply  36409  brcup  36410  brcap  36411  lemsuccf  36412  brrestrict  36422  dfrecs2  36423  dfrdg4  36424  fvtransport  36505  brcolinear2  36531  colineardim1  36534  brsegle  36581  fvline  36617  ellines  36625  nmulprop  36663  filnetlem3  36872  bj-inftyexpitaufo  37827  bj-inftyexpitaudisj  37830  bj-inftyexpiinv  37833  bj-inftyexpidisj  37835  bj-elccinfty  37839  bj-minftyccb  37850  finxpreclem2  38017  finxp0  38018  finxp1o  38019  finxpreclem3  38020  finxpreclem4  38021  finxpreclem5  38022  finxpreclem6  38023  poimirlem9  38261  poimirlem15  38267  poimirlem17  38269  poimirlem20  38272  poimirlem24  38276  poimirlem28  38280  mblfinlem2  38290  heiborlem6  38448  heiborlem7  38449  heiborlem8  38450  grposnOLD  38514  rngosn3  38556  gidsn  38584  zrdivrng  38585  brxrn  39013  ecxrn2  39038  br1cossxrnres  39168  dvhvaddval  41845  dvhvscaval  41854  dibglbN  41921  dihglbcpreN  42055  dihmeetlem4preN  42061  dihmeetlem13N  42074  hdmapfval  42582  elcnvlem  44310  cotrintab  44323  elimaint  44358  snhesn  44495  nregmodellem  45708  projf1o  45897  dvnprodlem1  46643  dvnprodlem2  46644  sge0xp  47126  hoicvr  47245  hoicvrrex  47253  hoidmv1le  47291  hoi2toco  47304  ovnlecvr2  47307  ovolval5lem2  47350  fsetsnf1  47772  setsidel  48108  prproropf1olem3  48237  prproropf1olem4  48238  prproropreud  48241  isisubgr  48610  ushggricedg  48675  gpgusgralem  48804  gpgvtxedg0  48811  gpgvtxedg1  48812  gpg5nbgrvtx03starlem1  48816  gpg5nbgrvtx03starlem2  48817  gpg5nbgrvtx03starlem3  48818  gpg5nbgrvtx13starlem1  48819  gpg5nbgrvtx13starlem2  48820  gpg5nbgrvtx13starlem3  48821  gpg3nbgrvtx0  48824  gpg3nbgrvtx0ALT  48825  gpg3nbgrvtx1  48826  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  gpg3kgrtriex  48837  gpgprismgr4cycllem2  48844  gpgprismgr4cycllem6  48848  gpgprismgr4cycllem7  48849  gpgprismgr4cycllem10  48852  gpg5edgnedg  48878  lmod1lem2  49251  lmod1lem3  49252  lmod1zr  49256  zlmodzxznm  49260  zlmodzxzldeplem  49261  rrx2xpref1o  49481  line2x  49517  inlinecirc02plem  49549  iinxp  49592  ovsng  49619  eloprab1st2nd  49629  tposid  49646  tposidres  49647  initc  49852  rescofuf  49854  idfurcl  49859  imaf1hom  49869  oppffn  49885  oppfvalg  49887  swapfval  50023  swapf1a  50030  swapf2a  50032  swapf1  50033  swapf2  50035  fucofvalg  50079  fucofval  50080  fucofvalne  50086  fuco21  50097  fucof21  50108  prcofvalg  50137  prcofvala  50138  prcofval  50139  thincciso  50214  setc1ocofval  50255  functermceu  50271  termcfuncval  50293  fucterm  50303  0fucterm  50304  relran  50385  ranval3  50392  ranrcl4lem  50399  ranup  50403  initocmd  50430