Theorem opex 5410

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 5235. (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 4569	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1144	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5374	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5261	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2836	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1092   ∈ wcel 2119  {cab 2718  Vcvv 3432  {csn 4562  {cpr 4564  ⟨cop 4568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-un 3895  df-in 3897  df-ss 3907  df-sn 4563  df-pr 4565  df-op 4569

This theorem is referenced by:  otex  5412  brv  5419  otth2  5430  otthg  5432  sbcop1  5435  oteqex2  5447  oteqex  5448  snopeqop  5454  propeqop  5455  propssopi  5456  euop2  5460  brsnop  5471  brtp  5472  opabidw  5473  opabid  5474  elopab  5476  rexopabb  5477  opabn0  5502  opeliunxp  5692  opeliun2xp  5693  elvvv  5701  opbrop  5723  relsnopg  5753  xpiindi  5784  raliunxp  5788  idrefALT  6070  intirr  6075  xpnz  6117  dmsnn0  6165  dmsnopg  6171  cnvcnvsn  6177  op2ndb  6185  opswap  6187  cnviin  6244  reuop  6251  dfpo2  6254  funopg  6526  dffv2  6929  fsn  7084  f1o2sn  7091  idref  7095  funsndifnop  7101  fmptsng  7119  fmptsnd  7120  fvsng  7131  resfunexg  7166  fveqf1o  7253  fliftel  7260  fliftel1  7261  oprabidw  7394  oprabid  7395  dfoprab2  7421  oprabv  7423  rnoprab  7468  eloprabga  7472  ot1stg  7952  ot2ndg  7953  ot3rdg  7954  fo1st  7958  fo2nd  7959  br1steqg  7960  br2ndeqg  7961  opiota  8008  eloprabi  8012  mposn  8049  fpar  8062  fsplitfpar  8064  opco1  8069  opco2  8070  frxp  8073  xporderlem  8074  fnwelem  8078  fvproj  8081  fimaproj  8082  xpord2lem  8089  xpord2pred  8092  xpord2indlem  8094  frxp3  8098  mpoxopoveq  8166  brtpos  8182  dmtpos  8185  rntpos  8186  tpostpos  8193  tfrlem11  8324  seqomlem1  8386  seqomlem3  8388  seqomlem4  8389  omeu  8517  naddcllem  8609  iiner  8733  xpsnen  8996  xpcomco  9002  xpassen  9006  xpmapenlem  9079  dif1en  9093  unxpdomlem1  9163  inlresf  9836  inrresf  9838  djur  9841  djuss  9842  djuun  9848  1stinl  9849  2ndinl  9850  1stinr  9851  2ndinr  9852  fseqenlem2  9945  dju1dif  10093  fpwwe  10567  addpipq2  10857  addpqnq  10859  mulpipq2  10860  mulpqnq  10862  ordpipq  10863  prlem934  10954  addcnsr  11056  mulcnsr  11057  ltresr  11061  addcnsrec  11064  mulcnsrec  11065  axcnre  11085  om2uzrdg  13916  uzrdg0i  13919  uzrdgsuci  13920  hashfun  14397  wrdexb  14485  s1len  14567  s1nz  14568  s111  14576  wrdlen2i  14902  brintclab  14961  fsumcnv  15733  fprodcnv  15946  ruclem1  16196  ruclem4  16199  eucalgval2  16548  crth  16746  phimullem  16747  setsval  17135  setsdm  17138  setsfun  17139  setsfun0  17140  setsexstruct2  17143  setsres  17146  setscom  17148  strfv  17171  setsid  17175  imasaddfnlem  17490  imasaddvallem  17491  imasvscafn  17499  idfuval  17841  cofuval  17847  resfval  17857  resfval2  17858  elhoma  17997  embedsetcestrclem  18121  xpcco  18147  xpcid  18153  1stfval  18155  2ndfval  18158  prfval  18163  prf1  18164  prf2  18166  evlfval  18181  curfval  18187  curf1  18189  curfcl  18196  hofval  18216  intopsn  18620  mgm1  18624  sgrp1  18695  mnd1  18745  mnd1id  18746  grpss  18928  grp1  19021  symg2bas  19366  efgmval  19685  efgi  19692  efgi2  19698  frgpnabllem1  19846  frgpnabllem2  19847  ring1  20289  rngqiprngimfv  21298  rngqiprngimf1  21300  opsrtoslem2  22039  mat1dimelbas  22461  mat1dimbas  22462  mat1dimscm  22465  mat1dimmul  22466  mat1f1o  22468  mat1rhmelval  22470  mvmulfval  22532  m2detleib  22621  txcnp  23610  upxp  23613  uptx  23615  txdis1cn  23625  hauseqlcld  23636  txlm  23638  xkoinjcn  23677  txflf  23996  qustgplem  24111  ucnima  24270  ucnprima  24271  fmucndlem  24280  imasdsf1olem  24363  cnheiborlem  24946  ovollb2lem  25480  ovolctb  25482  ovolshftlem1  25501  ovolscalem1  25505  ovolicc1  25508  ioombl1lem3  25552  ioombl1lem4  25553  ioorval  25566  dyadval  25584  mbfimaopnlem  25647  limccnp2  25884  addsval  27979  mulsval  28126  precsexlem1  28224  precsexlem2  28225  precsexlem3  28226  om2noseqrdg  28321  noseqrdg0  28324  noseqrdgsuc  28325  brbtwn  28993  brcgr  28994  eengbas  29075  ebtwntg  29076  ecgrtg  29077  elntg  29078  structvtxval  29115  structgrssvtx  29118  structgrssiedg  29119  gropd  29125  isuhgrop  29164  uhgrunop  29169  upgrop  29188  upgr0eop  29208  upgrunop  29213  umgrunop  29215  isuspgrop  29255  isusgrop  29256  ausgrusgrb  29259  usgr0eop  29340  griedg0ssusgr  29359  uhgrspanop  29390  uhgrspan1  29397  upgrres  29400  umgrres  29401  usgrres  29402  upgrres1  29407  umgrres1  29408  usgrres1  29409  usgrexi  29535  cusgrexi  29537  cffldtocusgr  29541  cusgrres  29542  vtxdgop  29564  umgr2v2e  29619  wlkp1lem2  29766  wlkswwlksf1o  29972  wwlksnext  29986  eupth2eucrct  30312  eupthvdres  30330  konigsbergumgr  30346  numclwwlk1lem2fv  30451  numclwlk1lem1  30464  ex-br  30526  ex-fpar  30557  cnnvg  30774  cnnvs  30776  cnnvnm  30777  h2hva  31070  h2hsm  31071  h2hnm  31072  hhssva  31353  hhsssm  31354  hhssnm  31355  hhshsslem1  31363  br8d  32707  xppreima2  32750  aciunf1lem  32761  ofpreima  32764  rlocaddval  33356  rlocmulval  33357  linds2eq  33471  selvply1rhmlema  33709  selvply1rhmlem1  33711  selvply1rhmlem2  33712  smatrcl  33987  smatlem  33988  txomap  34025  qtophaus  34027  hgt750lemb  34847  bnj97  35055  bnj553  35087  bnj966  35133  bnj1442  35238  erdszelem9  35434  erdszelem10  35435  txpconn  35467  txsconnlem  35475  goel  35582  goeleq12bg  35584  gonafv  35585  gonanegoal  35587  sat1el2xp  35614  fmlaomn0  35625  gonan0  35627  goaln0  35628  gonarlem  35629  gonar  35630  goalrlem  35631  goalr  35632  fmla0disjsuc  35633  fmlasucdisj  35634  satffunlem  35636  satffunlem1lem1  35637  satffunlem2lem1  35639  satfv0fvfmla0  35648  sategoelfvb  35654  prv1n  35666  msubval  35760  mvhval  35769  msubvrs  35795  brtpid1  35956  brtpid2  35957  brtpid3  35958  br8  35991  br6  35992  br4  35993  dfdm5  36008  dfrn5  36009  elima4  36011  fv1stcnv  36012  fv2ndcnv  36013  brtxp  36113  brpprod  36118  brpprod3b  36120  brsset  36122  brtxpsd  36127  dffun10  36147  elfuns  36148  brcart  36165  brimg  36170  brapply  36171  brcup  36172  brcap  36173  lemsuccf  36174  brrestrict  36184  dfrecs2  36185  dfrdg4  36186  fvtransport  36267  brcolinear2  36293  colineardim1  36296  brsegle  36343  fvline  36379  ellines  36387  filnetlem3  36615  bj-inftyexpitaufo  37569  bj-inftyexpitaudisj  37572  bj-inftyexpiinv  37575  bj-inftyexpidisj  37577  bj-elccinfty  37581  bj-minftyccb  37592  finxpreclem2  37759  finxp0  37760  finxp1o  37761  finxpreclem3  37762  finxpreclem4  37763  finxpreclem5  37764  finxpreclem6  37765  poimirlem9  38003  poimirlem15  38009  poimirlem17  38011  poimirlem20  38014  poimirlem24  38018  poimirlem28  38022  mblfinlem2  38032  heiborlem6  38190  heiborlem7  38191  heiborlem8  38192  grposnOLD  38256  rngosn3  38298  gidsn  38326  zrdivrng  38327  brxrn  38757  ecxrn2  38782  br1cossxrnres  38912  dvhvaddval  41589  dvhvscaval  41598  dibglbN  41665  dihglbcpreN  41799  dihmeetlem4preN  41805  dihmeetlem13N  41818  hdmapfval  42326  elcnvlem  44052  cotrintab  44065  elimaint  44100  snhesn  44237  nregmodellem  45467  projf1o  45650  dvnprodlem1  46396  dvnprodlem2  46397  sge0xp  46879  hoicvr  46998  hoicvrrex  47006  hoidmv1le  47044  hoi2toco  47057  ovnlecvr2  47060  ovolval5lem2  47103  fsetsnf1  47522  setsidel  47858  prproropf1olem3  47987  prproropf1olem4  47988  prproropreud  47991  isisubgr  48360  ushggricedg  48425  gpgusgralem  48554  gpgvtxedg0  48561  gpgvtxedg1  48562  gpg5nbgrvtx03starlem1  48566  gpg5nbgrvtx03starlem2  48567  gpg5nbgrvtx03starlem3  48568  gpg5nbgrvtx13starlem1  48569  gpg5nbgrvtx13starlem2  48570  gpg5nbgrvtx13starlem3  48571  gpg3nbgrvtx0  48574  gpg3nbgrvtx0ALT  48575  gpg3nbgrvtx1  48576  gpg5nbgrvtx03star  48578  gpg5nbgr3star  48579  gpg3kgrtriex  48587  gpgprismgr4cycllem2  48594  gpgprismgr4cycllem6  48598  gpgprismgr4cycllem7  48599  gpgprismgr4cycllem10  48602  gpg5edgnedg  48628  lmod1lem2  48986  lmod1lem3  48987  lmod1zr  48991  zlmodzxznm  48995  zlmodzxzldeplem  48996  rrx2xpref1o  49216  line2x  49252  inlinecirc02plem  49284  iinxp  49328  ovsng  49355  eloprab1st2nd  49365  tposid  49382  tposidres  49383  initc  49588  rescofuf  49590  idfurcl  49595  imaf1hom  49605  oppffn  49621  oppfvalg  49623  swapfval  49759  swapf1a  49766  swapf2a  49768  swapf1  49769  swapf2  49771  fucofvalg  49815  fucofval  49816  fucofvalne  49822  fuco21  49833  fucof21  49844  prcofvalg  49873  prcofvala  49874  prcofval  49875  thincciso  49950  setc1ocofval  49991  functermceu  50007  termcfuncval  50029  fucterm  50039  0fucterm  50040  relran  50121  ranval3  50128  ranrcl4lem  50135  ranup  50139  initocmd  50166