MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opex Structured version   Visualization version   GIF version

Theorem opex 5348
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.)
Assertion
Ref Expression
opex 𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex
StepHypRef Expression
1 dfopif 4794 . 2 𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2 prex 5324 . . 3 {{𝐴}, {𝐴, 𝐵}} ∈ V
3 0ex 5203 . . 3 ∅ ∈ V
42, 3ifex 4513 . 2 if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
51, 4eqeltri 2909 1 𝐴, 𝐵⟩ ∈ V
Colors of variables: wff setvar class
Syntax hints:  wa 396  wcel 2105  Vcvv 3495  c0 4290  ifcif 4465  {csn 4559  {cpr 4561  cop 4565
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793  ax-sep 5195  ax-nul 5202  ax-pr 5321
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566
This theorem is referenced by:  otex  5349  brv  5356  otth2  5367  otthg  5369  sbcop1  5371  oteqex2  5381  oteqex  5382  snopeqop  5388  propeqop  5389  propssopi  5390  euop2  5394  opabidw  5404  opabid  5405  elopab  5406  rexopabb  5407  opabn0  5432  opeliunxp  5613  elvvv  5621  opbrop  5642  relsnopg  5670  xpiindi  5700  raliunxp  5704  idrefALT  5967  intirr  5972  xpnz  6010  dmsnn0  6058  dmsnopg  6064  cnvcnvsn  6070  op2ndb  6078  opswap  6080  cnviin  6131  reuop  6138  funopg  6383  dffv2  6750  fsn  6890  f1o2sn  6897  idref  6901  funsndifnop  6906  fmptsng  6923  fmptsnd  6924  fvsng  6935  resfunexg  6970  fveqf1o  7049  fliftel  7051  fliftel1  7052  oprabidw  7176  oprabid  7177  dfoprab2  7201  oprabv  7203  rnoprab  7246  eloprabga  7250  ot1stg  7694  ot2ndg  7695  ot3rdg  7696  fo1st  7700  fo2nd  7701  br1steqg  7702  br2ndeqg  7703  opiota  7748  eloprabi  7752  mposn  7789  fpar  7802  fsplitfpar  7805  algrflem  7810  frxp  7811  xporderlem  7812  fnwelem  7816  fvproj  7819  fimaproj  7820  mpoxopoveq  7876  brtpos  7892  dmtpos  7895  rntpos  7896  tpostpos  7903  wfrlem14  7959  tfrlem11  8015  seqomlem1  8077  seqomlem3  8079  seqomlem4  8080  omeu  8201  iiner  8359  xpsnen  8590  xpcomco  8596  xpassen  8600  xpmapenlem  8673  unxpdomlem1  8711  inlresf  9332  inrresf  9334  djur  9337  djuss  9338  djuun  9344  1stinl  9345  2ndinl  9346  1stinr  9347  2ndinr  9348  fseqenlem2  9440  dju1dif  9587  fpwwe  10057  addpipq2  10347  addpqnq  10349  mulpipq2  10350  mulpqnq  10352  ordpipq  10353  prlem934  10444  addcnsr  10546  mulcnsr  10547  ltresr  10551  addcnsrec  10554  mulcnsrec  10555  axcnre  10575  om2uzrdg  13314  uzrdg0i  13317  uzrdgsuci  13318  hashfun  13788  wrdexb  13863  s1len  13950  s1nz  13951  s111  13959  wrdlen2i  14294  brintclab  14351  fsumcnv  15118  fprodcnv  15327  ruclem1  15574  ruclem4  15577  eucalgval2  15915  crth  16105  phimullem  16106  setsval  16503  setsdm  16507  setsfun  16508  setsfun0  16509  setsexstruct2  16512  setsres  16515  setscom  16517  strfv  16521  setsid  16528  imasaddfnlem  16791  imasaddvallem  16792  imasvscafn  16800  idfuval  17136  cofuval  17142  resfval  17152  resfval2  17153  elhoma  17282  embedsetcestrclem  17397  xpcco  17423  xpcid  17429  1stfval  17431  2ndfval  17434  prfval  17439  prf1  17440  prf2  17442  evlfval  17457  curfval  17463  curf1  17465  curfcl  17472  hofval  17492  intopsn  17854  mgm1  17858  sgrp1  17900  mnd1  17942  mnd1id  17943  grpss  18061  grp1  18146  symg2bas  18457  efgmval  18769  efgi  18776  efgi2  18782  frgpnabllem1  18924  frgpnabllem2  18925  ring1  19283  opsrtoslem2  20195  mat1dimelbas  21010  mat1dimbas  21011  mat1dimscm  21014  mat1dimmul  21015  mat1f1o  21017  mat1rhmelval  21019  mvmulfval  21081  m2detleib  21170  txcnp  22158  upxp  22161  uptx  22163  txdis1cn  22173  hauseqlcld  22184  txlm  22186  xkoinjcn  22225  txflf  22544  qustgplem  22658  ucnima  22819  ucnprima  22820  fmucndlem  22829  imasdsf1olem  22912  cnheiborlem  23487  ovollb2lem  24018  ovolctb  24020  ovolshftlem1  24039  ovolscalem1  24043  ovolicc1  24046  ioombl1lem3  24090  ioombl1lem4  24091  ioorval  24104  dyadval  24122  mbfimaopnlem  24185  limccnp2  24419  brbtwn  26613  brcgr  26614  eengbas  26695  ebtwntg  26696  ecgrtg  26697  elntg  26698  structvtxval  26734  structgrssvtx  26737  structgrssiedg  26738  gropd  26744  isuhgrop  26783  uhgrunop  26788  upgrop  26807  upgr0eop  26827  upgrunop  26832  umgrunop  26834  isuspgrop  26874  isusgrop  26875  ausgrusgrb  26878  usgr0eop  26956  usgrexmpl  26973  griedg0ssusgr  26975  uhgrspanop  27006  uhgrspan1  27013  upgrres  27016  umgrres  27017  usgrres  27018  upgrres1  27023  umgrres1  27024  usgrres1  27025  usgrexi  27151  cusgrexi  27153  cffldtocusgr  27157  cusgrres  27158  vtxdgop  27180  umgr2v2e  27235  wlkp1lem2  27384  wlkswwlksf1o  27585  wwlksnext  27599  eupth2eucrct  27924  eupthvdres  27942  konigsbergumgr  27958  numclwwlk1lem2fv  28063  numclwlk1lem1  28076  ex-br  28138  ex-fpar  28169  cnnvg  28383  cnnvs  28385  cnnvnm  28386  h2hva  28679  h2hsm  28680  h2hnm  28681  hhssva  28962  hhsssm  28963  hhssnm  28964  hhshsslem1  28972  br8d  30290  xppreima2  30324  aciunf1lem  30336  ofpreima  30339  brsnop  30356  cnvoprabOLD  30383  linds2eq  30869  smatrcl  30961  smatlem  30962  txomap  30998  qtophaus  31000  hgt750lemb  31827  bnj97  32038  bnj553  32070  bnj966  32116  bnj1442  32219  erdszelem9  32344  erdszelem10  32345  txpconn  32377  txsconnlem  32385  goel  32492  goeleq12bg  32494  gonafv  32495  gonanegoal  32497  sat1el2xp  32524  fmlaomn0  32535  gonan0  32537  goaln0  32538  gonarlem  32539  gonar  32540  goalrlem  32541  goalr  32542  fmla0disjsuc  32543  fmlasucdisj  32544  satffunlem  32546  satffunlem1lem1  32547  satffunlem2lem1  32549  satfv0fvfmla0  32558  sategoelfvb  32564  prv1n  32576  msubval  32670  mvhval  32679  msubvrs  32705  brtpid1  32849  brtpid2  32850  brtpid3  32851  brtp  32883  dfpo2  32889  br8  32890  br6  32891  br4  32892  dfdm5  32914  dfrn5  32915  elima4  32917  fv1stcnv  32918  fv2ndcnv  32919  brtxp  33239  brpprod  33244  brpprod3b  33246  brsset  33248  brtxpsd  33253  dffun10  33273  elfuns  33274  brcart  33291  brimg  33296  brapply  33297  brcup  33298  brcap  33299  brsuccf  33300  brrestrict  33308  dfrecs2  33309  dfrdg4  33310  fvtransport  33391  brcolinear2  33417  colineardim1  33420  brsegle  33467  fvline  33503  ellines  33511  filnetlem3  33626  bj-inftyexpitaufo  34377  bj-inftyexpitaudisj  34380  bj-inftyexpiinv  34383  bj-inftyexpidisj  34385  bj-elccinfty  34389  bj-minftyccb  34400  finxpreclem2  34554  finxp0  34555  finxp1o  34556  finxpreclem3  34557  finxpreclem4  34558  finxpreclem5  34559  finxpreclem6  34560  poimirlem9  34783  poimirlem15  34789  poimirlem17  34791  poimirlem20  34794  poimirlem24  34798  poimirlem28  34802  mblfinlem2  34812  heiborlem6  34977  heiborlem7  34978  heiborlem8  34979  grposnOLD  35043  rngosn3  35085  gidsn  35113  zrdivrng  35114  brxrn  35508  br1cossxrnres  35570  dvhvaddval  38108  dvhvscaval  38117  dibglbN  38184  dihglbcpreN  38318  dihmeetlem4preN  38324  dihmeetlem13N  38337  hdmapfval  38845  elcnvlem  39841  cotrintab  39854  elimaint  39873  snhesn  40012  projf1o  41339  dvnprodlem1  42111  dvnprodlem2  42112  sge0xp  42592  hoicvr  42711  hoicvrrex  42719  hoidmv1le  42757  hoi2toco  42770  ovnlecvr2  42773  ovolval5lem2  42816  setsidel  43417  prproropf1olem3  43514  prproropf1olem4  43515  prproropreud  43518  ushrisomgr  43853  opeliun2xp  44279  lmod1lem2  44441  lmod1lem3  44442  lmod1zr  44446  zlmodzxznm  44450  zlmodzxzldeplem  44451  rrx2xpref1o  44603  line2x  44639  inlinecirc02plem  44671
  Copyright terms: Public domain W3C validator