Theorem opex 5432

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 5260. (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 4591	. 2 ⊢ ⟨𝐴, 𝐵⟩ = {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})}
2		simp3 1156	. . 3 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}}) → 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})
3		prex 5396	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
4	2, 3	abex 5288	. 2 ⊢ {𝑥 ∣ (𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐴}, {𝐴, 𝐵}})} ∈ V
5	1, 4	eqeltri 2857	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

This proof depends on syntax axioms:   ∧ w3a 1103   ∈ wcel 2145  {cab 2739  Vcvv 3451  {csn 4584  {cpr 4586  ⟨cop 4590

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-un 3904  df-in 3906  df-ss 3916  df-sn 4585  df-pr 4587  df-op 4591

This theorem is used by:  otex  5434  brv  5441  otth2  5452  otthg  5454  sbcop1  5458  oteqex2  5471  oteqex  5472  snopeqop  5478  propeqop  5479  propssopi  5480  euop2  5485  brsnop  5496  brtp  5497  opabidw  5498  opabid  5499  elopab  5501  rexopabb  5502  opabn0  5528  opeliunxp  5718  opeliun2xp  5719  elvvv  5727  opbrop  5749  relsnopg  5781  xpiindi  5812  raliunxp  5816  idrefALT  6107  intirr  6112  xpnz  6150  dmsnn0  6207  dmsnopg  6213  cnvcnvsn  6219  op2ndb  6227  opswap  6229  cnviin  6288  reuop  6295  dfpo2  6298  funopg  6572  dffv2  6978  fsn  7134  f1o2sn  7143  idref  7147  funsndifnop  7153  fmptsng  7171  fmptsnd  7172  fvsng  7183  resfunexg  7219  fveqf1o  7308  fliftel  7315  fliftel1  7316  oprabidw  7449  oprabid  7450  dfoprab2  7476  oprabv  7478  rnoprab  7523  eloprabga  7527  ot1stg  8013  ot2ndg  8014  ot3rdg  8015  fo1st  8019  fo2nd  8020  br1steqg  8021  br2ndeqg  8022  opiota  8068  eloprabi  8072  mposn  8112  fpar  8125  fsplitfpar  8127  opco1  8132  opco2  8133  frxp  8136  xporderlem  8137  fnwelem  8141  fvproj  8144  fimaproj  8145  xpord2lem  8152  xpord2pred  8155  xpord2indlem  8157  frxp3  8161  mpoxopoveq  8229  brtpos  8245  dmtpos  8248  rntpos  8249  tpostpos  8256  tfrlem11  8389  seqomlem1  8453  seqomlem3  8455  seqomlem4  8456  omeu  8586  naddcllem  8678  iiner  8803  xpsnen  9073  xpcomco  9079  xpassen  9083  xpmapenlem  9156  dif1en  9170  unxpdomlem1  9240  inlresf  9988  inrresf  9990  djur  9993  djuss  9994  djuun  10000  1stinl  10001  2ndinl  10002  1stinr  10003  2ndinr  10004  fseqenlem2  10097  dju1dif  10244  fpwwe  10724  addpipq2  11014  addpqnq  11016  mulpipq2  11017  mulpqnq  11019  ordpipq  11020  prlem934  11111  addcnsr  11213  mulcnsr  11214  ltresr  11218  addcnsrec  11221  mulcnsrec  11222  axcnre  11242  om2uzrdg  14092  uzrdg0i  14095  uzrdgsuci  14096  hashfun  14575  wrdexb  14663  s1len  14746  s1nz  14747  s111  14756  wrdlen2i  15086  brintclab  15147  fsumcnv  15932  fprodcnv  16143  ruclem1  16392  ruclem4  16395  eucalgval2  16749  crth  16948  phimullem  16949  setsval  17338  setsdm  17341  setsfun  17342  setsfun0  17343  setsexstruct2  17346  setsres  17349  setscom  17351  strfv  17374  setsid  17378  imasaddfnlem  17693  imasaddvallem  17694  imasvscafn  17702  idfuval  18044  cofuval  18050  resfval  18060  resfval2  18061  elhoma  18200  embedsetcestrclem  18324  xpcco  18350  xpcid  18356  1stfval  18358  2ndfval  18361  prfval  18366  prf1  18367  prf2  18369  evlfval  18384  curfval  18390  curf1  18392  curfcl  18399  hofval  18419  intopsn  18825  mgm1  18829  sgrp1  18911  mnd1  18966  mnd1id  18967  degenmgm  19130  degenmgm2nfun  19132  degenmgm2  19133  grpss  19158  grp1  19250  symg2bas  19600  efgmval  19919  efgi  19926  efgi2  19932  frgpnabllem1  20080  frgpnabllem2  20081  ring1  20534  rngqiprngimfv  21587  rngqiprngimf1  21589  opsrtoslem2  22358  mat1dimelbas  22779  mat1dimbas  22780  mat1dimscm  22783  mat1dimmul  22784  mat1f1o  22786  mat1rhmelval  22788  mvmulfval  22850  m2detleib  22939  txcnp  23932  upxp  23935  uptx  23937  txdis1cn  23947  hauseqlcld  23958  txlm  23960  xkoinjcn  23999  txflf  24318  qustgplem  24433  ucnima  24592  ucnprima  24593  fmucndlem  24602  imasdsf1olem  24685  cnheiborlem  25268  ovollb2lem  25802  ovolctb  25804  ovolshftlem1  25823  ovolscalem1  25827  ovolicc1  25830  ioombl1lem3  25874  ioombl1lem4  25875  ioorval  25888  dyadval  25906  mbfimaopnlem  25969  limccnp2  26205  addsval  28341  mulsval  28488  precsexlem1  28586  precsexlem2  28587  precsexlem3  28588  om2noseqrdg  28683  noseqrdg0  28686  noseqrdgsuc  28687  brbtwn  29470  brcgr  29471  eengbas  29552  ebtwntg  29553  ecgrtg  29554  elntg  29555  structvtxval  29592  structgrssvtx  29595  structgrssiedg  29596  gropd  29602  isuhgrop  29641  uhgrunop  29646  upgrop  29665  upgr0eop  29685  upgrunop  29690  umgrunop  29692  isuspgrop  29735  isusgrop  29736  ausgrusgrb  29739  usgr0eop  29820  griedg0ssusgr  29839  uhgrspanop  29870  uhgrspan1  29877  upgrres  29880  umgrres  29881  usgrres  29882  upgrres1  29887  umgrres1  29888  usgrres1  29889  usgrexi  30015  cusgrexi  30017  cffldtocusgr  30021  cusgrres  30022  vtxdgop  30044  umgr2v2e  30099  wlkp1lem2  30246  wlkswwlksf1o  30461  wwlksnext  30475  eupth2eucrct  30811  eupthvdres  30829  konigsbergumgr  30845  numclwwlk1lem2fv  30950  numclwlk1lem1  30963  ex-br  31025  ex-fpar  31056  cnnvg  31273  cnnvs  31275  cnnvnm  31276  h2hva  31569  h2hsm  31570  h2hnm  31571  hhssva  31852  hhsssm  31853  hhssnm  31854  hhshsslem1  31862  br8d  33195  xppreima2  33238  aciunf1lem  33249  ofpreima  33252  rlocaddval  33823  rlocmulval  33824  linds2eq  33929  selvply1rhmlema  34143  selvply1rhmlem1  34145  selvply1rhmlem2  34146  smatrcl  34421  smatlem  34422  txomap  34459  qtophaus  34461  hgt750lemb  35278  bnj97  35489  bnj553  35521  bnj966  35567  bnj1442  35672  erdszelem9  35943  erdszelem10  35944  txpconn  35976  txsconnlem  35984  goel  36091  goeleq12bg  36093  gonafv  36094  gonanegoal  36096  sat1el2xp  36123  fmlaomn0  36134  gonan0  36136  goaln0  36137  gonarlem  36138  gonar  36139  goalrlem  36140  goalr  36141  fmla0disjsuc  36142  fmlasucdisj  36143  satffunlem  36145  satffunlem1lem1  36146  satffunlem2lem1  36148  satfv0fvfmla0  36157  sategoelfvb  36163  prv1n  36175  msubval  36269  mvhval  36278  msubvrs  36304  brtpid1  36465  brtpid2  36466  brtpid3  36467  br8  36500  br6  36501  br4  36502  dfdm5  36517  dfrn5  36518  elima4  36520  fv1stcnv  36521  fv2ndcnv  36522  brtxp  36622  brpprod  36627  brpprod3b  36629  brsset  36631  brtxpsd  36636  dffun10  36656  elfuns  36657  brcart  36674  brimg  36679  brapply  36680  brcup  36681  brcap  36682  lemsuccf  36683  brrestrict  36693  dfrecs2  36694  dfrdg4  36695  fvtransport  36777  brcolinear2  36803  colineardim1  36806  brsegle  36853  fvline  36889  ellines  36897  nmulprop  36919  filnetlem3  37148  bj-inftyexpitaufo  38103  bj-inftyexpitaudisj  38106  bj-inftyexpiinv  38109  bj-inftyexpidisj  38111  bj-elccinfty  38115  bj-minftyccb  38126  finxpreclem2  38293  finxp0  38294  finxp1o  38295  finxpreclem3  38296  finxpreclem4  38297  finxpreclem5  38298  finxpreclem6  38299  poimirlem9  38527  poimirlem15  38533  poimirlem17  38535  poimirlem20  38538  poimirlem24  38542  poimirlem28  38546  mblfinlem2  38556  heiborlem6  38730  heiborlem7  38731  heiborlem8  38732  grposnOLD  38796  rngosn3  38838  gidsn  38866  zrdivrng  38867  brxrn  39295  ecxrn2  39320  br1cossxrnres  39450  dvhvaddval  42127  dvhvscaval  42136  dibglbN  42203  dihglbcpreN  42337  dihmeetlem4preN  42343  dihmeetlem13N  42356  hdmapfval  42864  elcnvlem  44586  cotrintab  44599  elimaint  44634  snhesn  44771  nregmodellem  45984  projf1o  46180  dvnprodlem1  46925  dvnprodlem2  46926  sge0xp  47408  hoicvr  47527  hoicvrrex  47535  hoidmv1le  47573  hoi2toco  47586  ovnlecvr2  47589  ovolval5lem2  47632  fsetsnf1  48091  setsidel  48427  prproropf1olem3  48556  prproropf1olem4  48557  prproropreud  48560  isisubgr  48929  ushggricedg  48994  gpgusgralem  49123  gpgvtxedg0  49130  gpgvtxedg1  49131  gpg5nbgrvtx03starlem1  49135  gpg5nbgrvtx03starlem2  49136  gpg5nbgrvtx03starlem3  49137  gpg5nbgrvtx13starlem1  49138  gpg5nbgrvtx13starlem2  49139  gpg5nbgrvtx13starlem3  49140  gpg3nbgrvtx0  49143  gpg3nbgrvtx0ALT  49144  gpg3nbgrvtx1  49145  gpg5nbgrvtx03star  49147  gpg5nbgr3star  49148  gpg3kgrtriex  49156  gpgprismgr4cycllem2  49163  gpgprismgr4cycllem6  49167  gpgprismgr4cycllem7  49168  gpgprismgr4cycllem10  49171  gpg5edgnedg  49197  lmod1lem2  49569  lmod1lem3  49570  lmod1zr  49574  zlmodzxznm  49578  zlmodzxzldeplem  49579  rrx2xpref1o  49799  line2x  49835  inlinecirc02plem  49867  iinxp  49910  ovsng  49937  eloprab1st2nd  49947  tposid  49962  tposidres  49963  initc  50168  rescofuf  50170  idfurcl  50175  imaf1hom  50185  oppffn  50201  oppfvalg  50203  swapfval  50339  swapf1a  50346  swapf2a  50348  swapf1  50349  swapf2  50351  fucofvalg  50395  fucofval  50396  fucofvalne  50402  fuco21  50413  fucof21  50424  prcofvalg  50453  prcofvala  50454  prcofval  50455  thincciso  50530  setc1ocofval  50571  functermceu  50587  termcfuncval  50609  fucterm  50619  0fucterm  50620  relran  50701  ranval3  50708  ranrcl4lem  50715  ranup  50719  initocmd  50746