Theorem opex 5419

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 4589	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1139	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5384	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5273	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2833	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ w3a 1087   ∈ wcel 2114  {cab 2715  Vcvv 3442  {csn 4582  {cpr 4584  ⟨cop 4588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-un 3908  df-in 3910  df-ss 3920  df-sn 4583  df-pr 4585  df-op 4589

This theorem is referenced by:  otex  5421  brv  5428  otth2  5439  otthg  5441  sbcop1  5444  oteqex2  5455  oteqex  5456  snopeqop  5462  propeqop  5463  propssopi  5464  euop2  5468  brsnop  5478  brtp  5479  opabidw  5480  opabid  5481  elopab  5483  rexopabb  5484  opabn0  5509  opeliunxp  5699  opeliun2xp  5700  elvvv  5708  opbrop  5730  relsnopg  5760  xpiindi  5792  raliunxp  5796  idrefALT  6078  intirr  6083  xpnz  6125  dmsnn0  6173  dmsnopg  6179  cnvcnvsn  6185  op2ndb  6193  opswap  6195  cnviin  6252  reuop  6259  dfpo2  6262  funopg  6534  dffv2  6937  fsn  7090  f1o2sn  7097  idref  7101  funsndifnop  7106  fmptsng  7124  fmptsnd  7125  fvsng  7136  resfunexg  7171  fveqf1o  7258  fliftel  7265  fliftel1  7266  oprabidw  7399  oprabid  7400  dfoprab2  7426  oprabv  7428  rnoprab  7473  eloprabga  7477  ot1stg  7957  ot2ndg  7958  ot3rdg  7959  fo1st  7963  fo2nd  7964  br1steqg  7965  br2ndeqg  7966  opiota  8013  eloprabi  8017  mposn  8055  fpar  8068  fsplitfpar  8070  opco1  8075  opco2  8076  frxp  8078  xporderlem  8079  fnwelem  8083  fvproj  8086  fimaproj  8087  xpord2lem  8094  xpord2pred  8097  xpord2indlem  8099  frxp3  8103  mpoxopoveq  8171  brtpos  8187  dmtpos  8190  rntpos  8191  tpostpos  8198  tfrlem11  8329  seqomlem1  8391  seqomlem3  8393  seqomlem4  8394  omeu  8522  naddcllem  8614  iiner  8738  xpsnen  9001  xpcomco  9007  xpassen  9011  xpmapenlem  9084  dif1en  9098  unxpdomlem1  9168  inlresf  9838  inrresf  9840  djur  9843  djuss  9844  djuun  9850  1stinl  9851  2ndinl  9852  1stinr  9853  2ndinr  9854  fseqenlem2  9947  dju1dif  10095  fpwwe  10569  addpipq2  10859  addpqnq  10861  mulpipq2  10862  mulpqnq  10864  ordpipq  10865  prlem934  10956  addcnsr  11058  mulcnsr  11059  ltresr  11063  addcnsrec  11066  mulcnsrec  11067  axcnre  11087  om2uzrdg  13891  uzrdg0i  13894  uzrdgsuci  13895  hashfun  14372  wrdexb  14460  s1len  14542  s1nz  14543  s111  14551  wrdlen2i  14877  brintclab  14936  fsumcnv  15708  fprodcnv  15918  ruclem1  16168  ruclem4  16171  eucalgval2  16520  crth  16717  phimullem  16718  setsval  17106  setsdm  17109  setsfun  17110  setsfun0  17111  setsexstruct2  17114  setsres  17117  setscom  17119  strfv  17142  setsid  17146  imasaddfnlem  17461  imasaddvallem  17462  imasvscafn  17470  idfuval  17812  cofuval  17818  resfval  17828  resfval2  17829  elhoma  17968  embedsetcestrclem  18092  xpcco  18118  xpcid  18124  1stfval  18126  2ndfval  18129  prfval  18134  prf1  18135  prf2  18137  evlfval  18152  curfval  18158  curf1  18160  curfcl  18167  hofval  18187  intopsn  18591  mgm1  18595  sgrp1  18666  mnd1  18716  mnd1id  18717  grpss  18896  grp1  18989  symg2bas  19334  efgmval  19653  efgi  19660  efgi2  19666  frgpnabllem1  19814  frgpnabllem2  19815  ring1  20257  rngqiprngimfv  21265  rngqiprngimf1  21267  opsrtoslem2  22023  mat1dimelbas  22427  mat1dimbas  22428  mat1dimscm  22431  mat1dimmul  22432  mat1f1o  22434  mat1rhmelval  22436  mvmulfval  22498  m2detleib  22587  txcnp  23576  upxp  23579  uptx  23581  txdis1cn  23591  hauseqlcld  23602  txlm  23604  xkoinjcn  23643  txflf  23962  qustgplem  24077  ucnima  24236  ucnprima  24237  fmucndlem  24246  imasdsf1olem  24329  cnheiborlem  24921  ovollb2lem  25457  ovolctb  25459  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  ioombl1lem3  25529  ioombl1lem4  25530  ioorval  25543  dyadval  25561  mbfimaopnlem  25624  limccnp2  25861  addsval  27970  mulsval  28117  precsexlem1  28215  precsexlem2  28216  precsexlem3  28217  om2noseqrdg  28312  noseqrdg0  28315  noseqrdgsuc  28316  brbtwn  28984  brcgr  28985  eengbas  29066  ebtwntg  29067  ecgrtg  29068  elntg  29069  structvtxval  29106  structgrssvtx  29109  structgrssiedg  29110  gropd  29116  isuhgrop  29155  uhgrunop  29160  upgrop  29179  upgr0eop  29199  upgrunop  29204  umgrunop  29206  isuspgrop  29246  isusgrop  29247  ausgrusgrb  29250  usgr0eop  29331  griedg0ssusgr  29350  uhgrspanop  29381  uhgrspan1  29388  upgrres  29391  umgrres  29392  usgrres  29393  upgrres1  29398  umgrres1  29399  usgrres1  29400  usgrexi  29526  cusgrexi  29528  cffldtocusgr  29532  cffldtocusgrOLD  29533  cusgrres  29534  vtxdgop  29556  umgr2v2e  29611  wlkp1lem2  29758  wlkswwlksf1o  29964  wwlksnext  29978  eupth2eucrct  30304  eupthvdres  30322  konigsbergumgr  30338  numclwwlk1lem2fv  30443  numclwlk1lem1  30456  ex-br  30518  ex-fpar  30549  cnnvg  30765  cnnvs  30767  cnnvnm  30768  h2hva  31061  h2hsm  31062  h2hnm  31063  hhssva  31344  hhsssm  31345  hhssnm  31346  hhshsslem1  31354  br8d  32697  xppreima2  32740  aciunf1lem  32751  ofpreima  32754  rlocaddval  33361  rlocmulval  33362  linds2eq  33473  smatrcl  33973  smatlem  33974  txomap  34011  qtophaus  34013  hgt750lemb  34833  bnj97  35041  bnj553  35073  bnj966  35119  bnj1442  35224  erdszelem9  35412  erdszelem10  35413  txpconn  35445  txsconnlem  35453  goel  35560  goeleq12bg  35562  gonafv  35563  gonanegoal  35565  sat1el2xp  35592  fmlaomn0  35603  gonan0  35605  goaln0  35606  gonarlem  35607  gonar  35608  goalrlem  35609  goalr  35610  fmla0disjsuc  35611  fmlasucdisj  35612  satffunlem  35614  satffunlem1lem1  35615  satffunlem2lem1  35617  satfv0fvfmla0  35626  sategoelfvb  35632  prv1n  35644  msubval  35738  mvhval  35747  msubvrs  35773  brtpid1  35934  brtpid2  35935  brtpid3  35936  br8  35969  br6  35970  br4  35971  dfdm5  35986  dfrn5  35987  elima4  35989  fv1stcnv  35990  fv2ndcnv  35991  brtxp  36091  brpprod  36096  brpprod3b  36098  brsset  36100  brtxpsd  36105  dffun10  36125  elfuns  36126  brcart  36143  brimg  36148  brapply  36149  brcup  36150  brcap  36151  lemsuccf  36152  brrestrict  36162  dfrecs2  36163  dfrdg4  36164  fvtransport  36245  brcolinear2  36271  colineardim1  36274  brsegle  36321  fvline  36357  ellines  36365  filnetlem3  36593  bj-inftyexpitaufo  37454  bj-inftyexpitaudisj  37457  bj-inftyexpiinv  37460  bj-inftyexpidisj  37462  bj-elccinfty  37466  bj-minftyccb  37477  finxpreclem2  37642  finxp0  37643  finxp1o  37644  finxpreclem3  37645  finxpreclem4  37646  finxpreclem5  37647  finxpreclem6  37648  poimirlem9  37877  poimirlem15  37883  poimirlem17  37885  poimirlem20  37888  poimirlem24  37892  poimirlem28  37896  mblfinlem2  37906  heiborlem6  38064  heiborlem7  38065  heiborlem8  38066  grposnOLD  38130  rngosn3  38172  gidsn  38200  zrdivrng  38201  brxrn  38631  ecxrn2  38656  br1cossxrnres  38786  dvhvaddval  41463  dvhvscaval  41472  dibglbN  41539  dihglbcpreN  41673  dihmeetlem4preN  41679  dihmeetlem13N  41692  hdmapfval  42200  elcnvlem  43954  cotrintab  43967  elimaint  44002  snhesn  44139  nregmodellem  45369  projf1o  45552  dvnprodlem1  46301  dvnprodlem2  46302  sge0xp  46784  hoicvr  46903  hoicvrrex  46911  hoidmv1le  46949  hoi2toco  46962  ovnlecvr2  46965  ovolval5lem2  47008  fsetsnf1  47409  setsidel  47733  prproropf1olem3  47862  prproropf1olem4  47863  prproropreud  47866  isisubgr  48219  ushggricedg  48284  gpgusgralem  48413  gpgvtxedg0  48420  gpgvtxedg1  48421  gpg5nbgrvtx03starlem1  48425  gpg5nbgrvtx03starlem2  48426  gpg5nbgrvtx03starlem3  48427  gpg5nbgrvtx13starlem1  48428  gpg5nbgrvtx13starlem2  48429  gpg5nbgrvtx13starlem3  48430  gpg3nbgrvtx0  48433  gpg3nbgrvtx0ALT  48434  gpg3nbgrvtx1  48435  gpg5nbgrvtx03star  48437  gpg5nbgr3star  48438  gpg3kgrtriex  48446  gpgprismgr4cycllem2  48453  gpgprismgr4cycllem6  48457  gpgprismgr4cycllem7  48458  gpgprismgr4cycllem10  48461  gpg5edgnedg  48487  lmod1lem2  48845  lmod1lem3  48846  lmod1zr  48850  zlmodzxznm  48854  zlmodzxzldeplem  48855  rrx2xpref1o  49075  line2x  49111  inlinecirc02plem  49143  iinxp  49187  ovsng  49214  eloprab1st2nd  49224  tposid  49241  tposidres  49242  initc  49447  rescofuf  49449  idfurcl  49454  imaf1hom  49464  oppffn  49480  oppfvalg  49482  swapfval  49618  swapf1a  49625  swapf2a  49627  swapf1  49628  swapf2  49630  fucofvalg  49674  fucofval  49675  fucofvalne  49681  fuco21  49692  fucof21  49703  prcofvalg  49732  prcofvala  49733  prcofval  49734  thincciso  49809  setc1ocofval  49850  functermceu  49866  termcfuncval  49888  fucterm  49898  0fucterm  49899  relran  49980  ranval3  49987  ranrcl4lem  49994  ranup  49998  initocmd  50025