Theorem opex 5443

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 5268. (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 4598	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1154	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5407	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5294	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2865	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1101   ∈ wcel 2149  {cab 2747  Vcvv 3463  {csn 4591  {cpr 4593  ⟨cop 4597

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741  ax-sep 5258  ax-pr 5402

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-un 3918  df-in 3920  df-ss 3930  df-sn 4592  df-pr 4594  df-op 4598

This theorem is referenced by:  otex  5445  brv  5452  otth2  5463  otthg  5465  sbcop1  5468  oteqex2  5480  oteqex  5481  snopeqop  5487  propeqop  5488  propssopi  5489  euop2  5493  brsnop  5504  brtp  5505  opabidw  5506  opabid  5507  elopab  5509  rexopabb  5510  opabn0  5536  opeliunxp  5726  opeliun2xp  5727  elvvv  5735  opbrop  5757  relsnopg  5788  xpiindi  5819  raliunxp  5823  idrefALT  6111  intirr  6116  xpnz  6154  dmsnn0  6206  dmsnopg  6212  cnvcnvsn  6218  op2ndb  6226  opswap  6228  cnviin  6285  reuop  6292  dfpo2  6295  funopg  6568  dffv2  6974  fsn  7129  f1o2sn  7136  idref  7140  funsndifnop  7146  fmptsng  7164  fmptsnd  7165  fvsng  7176  resfunexg  7211  fveqf1o  7298  fliftel  7305  fliftel1  7306  oprabidw  7439  oprabid  7440  dfoprab2  7466  oprabv  7468  rnoprab  7513  eloprabga  7517  ot1stg  7996  ot2ndg  7997  ot3rdg  7998  fo1st  8002  fo2nd  8003  br1steqg  8004  br2ndeqg  8005  opiota  8052  eloprabi  8056  mposn  8094  fpar  8107  fsplitfpar  8109  opco1  8114  opco2  8115  frxp  8118  xporderlem  8119  fnwelem  8123  fvproj  8126  fimaproj  8127  xpord2lem  8134  xpord2pred  8137  xpord2indlem  8139  frxp3  8143  mpoxopoveq  8211  brtpos  8227  dmtpos  8230  rntpos  8231  tpostpos  8238  tfrlem11  8371  seqomlem1  8433  seqomlem3  8435  seqomlem4  8436  omeu  8566  naddcllem  8658  iiner  8783  xpsnen  9045  xpcomco  9051  xpassen  9055  xpmapenlem  9128  dif1en  9142  unxpdomlem1  9212  inlresf  9896  inrresf  9898  djur  9901  djuss  9902  djuun  9908  1stinl  9909  2ndinl  9910  1stinr  9911  2ndinr  9912  fseqenlem2  10005  dju1dif  10152  fpwwe  10627  addpipq2  10917  addpqnq  10919  mulpipq2  10920  mulpqnq  10922  ordpipq  10923  prlem934  11014  addcnsr  11116  mulcnsr  11117  ltresr  11121  addcnsrec  11124  mulcnsrec  11125  axcnre  11145  om2uzrdg  13988  uzrdg0i  13991  uzrdgsuci  13992  hashfun  14470  wrdexb  14558  s1len  14640  s1nz  14641  s111  14649  wrdlen2i  14975  brintclab  15034  fsumcnv  15820  fprodcnv  16033  ruclem1  16283  ruclem4  16286  eucalgval2  16635  crth  16833  phimullem  16834  setsval  17223  setsdm  17226  setsfun  17227  setsfun0  17228  setsexstruct2  17231  setsres  17234  setscom  17236  strfv  17259  setsid  17263  imasaddfnlem  17578  imasaddvallem  17579  imasvscafn  17587  idfuval  17929  cofuval  17935  resfval  17945  resfval2  17946  elhoma  18085  embedsetcestrclem  18209  xpcco  18235  xpcid  18241  1stfval  18243  2ndfval  18246  prfval  18251  prf1  18252  prf2  18254  evlfval  18269  curfval  18275  curf1  18277  curfcl  18284  hofval  18304  intopsn  18708  mgm1  18712  sgrp1  18783  mnd1  18833  mnd1id  18834  grpss  19017  grp1  19109  symg2bas  19459  efgmval  19778  efgi  19785  efgi2  19791  frgpnabllem1  19939  frgpnabllem2  19940  ring1  20389  rngqiprngimfv  21405  rngqiprngimf1  21407  opsrtoslem2  22172  mat1dimelbas  22593  mat1dimbas  22594  mat1dimscm  22597  mat1dimmul  22598  mat1f1o  22600  mat1rhmelval  22602  mvmulfval  22664  m2detleib  22753  txcnp  23742  upxp  23745  uptx  23747  txdis1cn  23757  hauseqlcld  23768  txlm  23770  xkoinjcn  23809  txflf  24128  qustgplem  24243  ucnima  24402  ucnprima  24403  fmucndlem  24412  imasdsf1olem  24495  cnheiborlem  25078  ovollb2lem  25612  ovolctb  25614  ovolshftlem1  25633  ovolscalem1  25637  ovolicc1  25640  ioombl1lem3  25684  ioombl1lem4  25685  ioorval  25698  dyadval  25716  mbfimaopnlem  25779  limccnp2  26016  addsval  28117  mulsval  28264  precsexlem1  28362  precsexlem2  28363  precsexlem3  28364  om2noseqrdg  28459  noseqrdg0  28462  noseqrdgsuc  28463  brbtwn  29186  brcgr  29187  eengbas  29268  ebtwntg  29269  ecgrtg  29270  elntg  29271  structvtxval  29308  structgrssvtx  29311  structgrssiedg  29312  gropd  29318  isuhgrop  29357  uhgrunop  29362  upgrop  29381  upgr0eop  29401  upgrunop  29406  umgrunop  29408  isuspgrop  29448  isusgrop  29449  ausgrusgrb  29452  usgr0eop  29533  griedg0ssusgr  29552  uhgrspanop  29583  uhgrspan1  29590  upgrres  29593  umgrres  29594  usgrres  29595  upgrres1  29600  umgrres1  29601  usgrres1  29602  usgrexi  29728  cusgrexi  29730  cffldtocusgr  29734  cusgrres  29735  vtxdgop  29757  umgr2v2e  29812  wlkp1lem2  29959  wlkswwlksf1o  30165  wwlksnext  30179  eupth2eucrct  30505  eupthvdres  30523  konigsbergumgr  30539  numclwwlk1lem2fv  30644  numclwlk1lem1  30657  ex-br  30719  ex-fpar  30750  cnnvg  30967  cnnvs  30969  cnnvnm  30970  h2hva  31263  h2hsm  31264  h2hnm  31265  hhssva  31546  hhsssm  31547  hhssnm  31548  hhshsslem1  31556  br8d  32890  xppreima2  32933  aciunf1lem  32944  ofpreima  32947  rlocaddval  33526  rlocmulval  33527  linds2eq  33634  selvply1rhmlema  33849  selvply1rhmlem1  33851  selvply1rhmlem2  33852  smatrcl  34127  smatlem  34128  txomap  34165  qtophaus  34167  hgt750lemb  34984  bnj97  35195  bnj553  35227  bnj966  35273  bnj1442  35378  erdszelem9  35586  erdszelem10  35587  txpconn  35619  txsconnlem  35627  goel  35734  goeleq12bg  35736  gonafv  35737  gonanegoal  35739  sat1el2xp  35766  fmlaomn0  35777  gonan0  35779  goaln0  35780  gonarlem  35781  gonar  35782  goalrlem  35783  goalr  35784  fmla0disjsuc  35785  fmlasucdisj  35786  satffunlem  35788  satffunlem1lem1  35789  satffunlem2lem1  35791  satfv0fvfmla0  35800  sategoelfvb  35806  prv1n  35818  msubval  35912  mvhval  35921  msubvrs  35947  brtpid1  36108  brtpid2  36109  brtpid3  36110  br8  36143  br6  36144  br4  36145  dfdm5  36160  dfrn5  36161  elima4  36163  fv1stcnv  36164  fv2ndcnv  36165  brtxp  36265  brpprod  36270  brpprod3b  36272  brsset  36274  brtxpsd  36279  dffun10  36299  elfuns  36300  brcart  36317  brimg  36322  brapply  36323  brcup  36324  brcap  36325  lemsuccf  36326  brrestrict  36336  dfrecs2  36337  dfrdg4  36338  fvtransport  36419  brcolinear2  36445  colineardim1  36448  brsegle  36495  fvline  36531  ellines  36539  nmulprop  36577  filnetlem3  36776  bj-inftyexpitaufo  37729  bj-inftyexpitaudisj  37732  bj-inftyexpiinv  37735  bj-inftyexpidisj  37737  bj-elccinfty  37741  bj-minftyccb  37752  finxpreclem2  37919  finxp0  37920  finxp1o  37921  finxpreclem3  37922  finxpreclem4  37923  finxpreclem5  37924  finxpreclem6  37925  poimirlem9  38163  poimirlem15  38169  poimirlem17  38171  poimirlem20  38174  poimirlem24  38178  poimirlem28  38182  mblfinlem2  38192  heiborlem6  38350  heiborlem7  38351  heiborlem8  38352  grposnOLD  38416  rngosn3  38458  gidsn  38486  zrdivrng  38487  brxrn  38917  ecxrn2  38942  br1cossxrnres  39072  dvhvaddval  41749  dvhvscaval  41758  dibglbN  41825  dihglbcpreN  41959  dihmeetlem4preN  41965  dihmeetlem13N  41978  hdmapfval  42486  elcnvlem  44214  cotrintab  44227  elimaint  44262  snhesn  44399  nregmodellem  45612  projf1o  45801  dvnprodlem1  46547  dvnprodlem2  46548  sge0xp  47030  hoicvr  47149  hoicvrrex  47157  hoidmv1le  47195  hoi2toco  47208  ovnlecvr2  47211  ovolval5lem2  47254  fsetsnf1  47673  setsidel  48009  prproropf1olem3  48138  prproropf1olem4  48139  prproropreud  48142  isisubgr  48511  ushggricedg  48576  gpgusgralem  48705  gpgvtxedg0  48712  gpgvtxedg1  48713  gpg5nbgrvtx03starlem1  48717  gpg5nbgrvtx03starlem2  48718  gpg5nbgrvtx03starlem3  48719  gpg5nbgrvtx13starlem1  48720  gpg5nbgrvtx13starlem2  48721  gpg5nbgrvtx13starlem3  48722  gpg3nbgrvtx0  48725  gpg3nbgrvtx0ALT  48726  gpg3nbgrvtx1  48727  gpg5nbgrvtx03star  48729  gpg5nbgr3star  48730  gpg3kgrtriex  48738  gpgprismgr4cycllem2  48745  gpgprismgr4cycllem6  48749  gpgprismgr4cycllem7  48750  gpgprismgr4cycllem10  48753  gpg5edgnedg  48779  lmod1lem2  49148  lmod1lem3  49149  lmod1zr  49153  zlmodzxznm  49157  zlmodzxzldeplem  49158  rrx2xpref1o  49378  line2x  49414  inlinecirc02plem  49446  iinxp  49489  ovsng  49516  eloprab1st2nd  49526  tposid  49543  tposidres  49544  initc  49749  rescofuf  49751  idfurcl  49756  imaf1hom  49766  oppffn  49782  oppfvalg  49784  swapfval  49920  swapf1a  49927  swapf2a  49929  swapf1  49930  swapf2  49932  fucofvalg  49976  fucofval  49977  fucofvalne  49983  fuco21  49994  fucof21  50005  prcofvalg  50034  prcofvala  50035  prcofval  50036  thincciso  50111  setc1ocofval  50152  functermceu  50168  termcfuncval  50190  fucterm  50200  0fucterm  50201  relran  50282  ranval3  50289  ranrcl4lem  50296  ranup  50300  initocmd  50327