MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  eqeltri Unicode version

Theorem eqeltri 2366
Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
eqeltr.1  |-  A  =  B
eqeltr.2  |-  B  e.  C
Assertion
Ref Expression
eqeltri  |-  A  e.  C

Proof of Theorem eqeltri
StepHypRef Expression
1 eqeltr.2 . 2  |-  B  e.  C
2 eqeltr.1 . . 3  |-  A  =  B
32eleq1i 2359 . 2  |-  ( A  e.  C  <->  B  e.  C )
41, 3mpbir 200 1  |-  A  e.  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696
This theorem is referenced by:  eqeltrri  2367  3eltr4i  2375  intab  3908  inex2  4172  pwex  4209  ord3ex  4216  zfpair  4228  opex  4253  otex  4254  uniopel  4286  tpex  4535  unisn2  4538  elvvuni  4766  isarep2  5348  fvex  5555  abrexex2  5796  ovex  5899  oprabex  5977  oprabrexex2  5979  riotaex  6324  tfrlem16  6425  1on  6502  2on  6503  3on  6505  4on  6506  oesuclem  6540  oecl  6552  nnecl  6627  1onn  6653  2onn  6654  3onn  6655  4onn  6656  mapsnf1o2  6831  map1  6955  sbthlem10  6996  map2xp  7047  nnunifi  7124  xpfi  7144  prfi  7147  tpfi  7148  fnfi  7150  pwfi  7167  inf0  7338  oancom  7368  cantnffval  7380  cantnfvalf  7382  oemapwe  7412  cantnffval2  7413  cnfcom2  7421  cnfcom3lem  7422  cnfcom3  7423  cnfcom3clem  7424  r1fin  7461  hta  7583  infxpenlem  7657  alephon  7712  alephfplem1  7747  dfac5lem4  7769  dfac5lem5  7770  kmlem10  7801  fin1a2lem10  8051  fin1a2lem12  8053  hsmexlem9  8067  axcc2lem  8078  domtriomlem  8084  axdc2lem  8090  axcclem  8099  brdom7disj  8172  brdom6disj  8173  iundom2g  8178  konigthlem  8206  canthwelem  8288  wunex2  8376  wunex3  8379  nqex  8563  1nq  8568  1pr  8655  axcnex  8785  ax1cn  8787  negex  9066  inelr  9752  cju  9758  nnexALT  9764  2re  9831  3re  9833  4re  9835  5re  9837  6re  9838  7re  9839  8re  9840  9re  9841  10re  9842  2nn  9893  3nn  9894  4nn  9895  5nn  9896  6nn  9897  7nn  9898  8nn  9899  9nn  9900  10nn  9901  nn0ex  9987  zexALT  10058  nneo  10111  zeo  10113  decex  10142  decnncl  10153  deccl  10154  numnncl2  10157  decnncl2  10158  numsucc  10166  numma2c  10173  numadd  10174  numaddc  10175  nummul1c  10176  nummul2c  10177  qexALT  10347  xrex  10367  pnfxr  10471  mnfxr  10472  xnegex  10551  xnegcl  10556  ixxssxr  10684  om2uzuzi  11028  ltweuz  11040  axdc4uzlem  11060  seqex  11064  m1expcl2  11141  faccl  11314  facwordi  11318  faclbnd2  11320  bccl  11350  hashunlei  11393  hashpw  11404  s1cli  11459  cats1un  11492  revs1  11499  cats1cli  11523  cats1fvn  11524  crre  11615  remim  11618  climmpt  12061  climle  12129  climsup  12159  sumex  12176  iserabs  12289  isumshft  12314  supcvg  12330  explecnv  12339  geo2lim  12347  ere  12386  eftlub  12405  efsep  12406  tan0  12447  ef01bndlem  12480  divalglem5  12612  divalglem9  12616  sadcf  12660  smupf  12685  crt  12862  phimullem  12863  eulerthlem2  12866  pczpre  12916  pockthi  12970  prmreclem2  12980  igz  12997  0ramcl  13086  1259lem1  13145  1259lem2  13146  1259lem3  13147  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem1  13151  2503lem2  13152  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  ndxarg  13184  ressbas  13214  ressbas2  13215  ressid  13219  strle1  13255  topnid  13356  prdsbasex  13367  prdsplusg  13374  prdsmulr  13375  prdsvsca  13376  prdsle  13377  prdsds  13379  prdshom  13382  prdsco  13383  pwselbasb  13403  pwsvscafval  13409  pwssca  13411  pwssnf1o  13413  imassca  13438  imasvsca  13439  imasle  13441  xpslem  13491  xpssca  13496  xpsvsca  13497  isacs2  13571  cidfval  13594  homffval  13610  comfffval  13617  oppchomfval  13633  oppccofval  13635  oppccatid  13638  monfval  13651  oppcmon  13657  sectffval  13669  invffval  13676  isoval  13683  rescbas  13722  reschom  13723  rescco  13725  subccatid  13736  fullsubc  13740  isfunc  13754  isfuncd  13755  idfu2nd  13767  idfu1st  13769  cofu1st  13773  cofu2nd  13775  funcres2c  13791  ressffth  13828  fuccofval  13849  fuchom  13851  fucco  13852  fuccatid  13859  fucid  13861  invfuc  13864  homafval  13877  arwval  13891  idafval  13905  coafval  13912  coapm  13919  setccatid  13932  catchomfval  13946  catccofval  13948  catccatid  13950  xpcbas  13968  xpchomfval  13969  xpccofval  13972  xpccatid  13978  1stf1  13982  1stf2  13983  2ndf1  13985  2ndf2  13986  prf1  13990  prf2fval  13991  evlf2  14008  evlf1  14010  curf1fval  14014  curf11  14016  curf12  14017  curf1cl  14018  curf2  14019  curf2cl  14021  hof2fval  14045  yonedalem4a  14065  yonedalem4c  14067  yonedalem3  14070  yonedainv  14071  isdrs  14084  ispos  14097  isposix  14107  pltfval  14109  lubfval  14128  lubval  14129  lubprop  14130  glbfval  14133  glbval  14134  glbprop  14135  joinfval  14137  joinlem  14140  meetfval  14144  meetlem  14147  clatlem  14232  isglbd  14237  odupos  14255  oduglb  14259  odumeet  14260  odulub  14261  odujoin  14262  ipolt  14278  ipopos  14279  isacs4lem  14287  isdlat  14312  plusffval  14395  issubmnd  14417  ismhm  14433  0mhm  14451  submacs  14458  pwsdiagmhm  14461  gsumvalx  14467  gsumval  14468  gsumress  14470  gsumz  14474  frmdplusg  14492  grpinvfval  14536  grpsubfval  14540  grplactfval  14578  mulgfval  14584  mulgval  14585  issubg  14637  0subg  14658  subgacs  14668  nsgacs  14669  nmznsg  14677  eqgfval  14681  eqgen  14686  isghm  14699  gicen  14757  isga  14761  subgga  14770  orbstafun  14781  orbstaval  14782  orbsta  14783  orbsta2  14784  symgplusg  14792  cayleylem2  14804  cntzfval  14812  cntzval  14813  oppgplusfval  14837  odfval  14864  odval  14865  odinf  14892  dfod2  14893  pgpfi1  14922  pgp0  14923  sylow1lem2  14926  sylow2alem2  14945  sylow2blem1  14947  sylow2blem2  14948  sylow3lem6  14959  lsmfval  14965  lsmvalx  14966  oppglsm  14969  pj1fval  15019  efglem  15041  efgtf  15047  efgsval2  15058  efgsp1  15062  efgrelexlemb  15075  efgcpbllemb  15080  frgpeccl  15086  frgpmhm  15090  vrgpval  15092  frgpuplem  15097  frgpupf  15098  frgpupval  15099  frgpup1  15100  frgpup3lem  15102  frgpnabllem1  15177  frgpnabllem2  15178  iscygodd  15191  prmcyg  15196  lt6abl  15197  dprdfeq0  15273  dmdprdsplitlem  15288  ablfacrplem  15316  ablfacrp  15317  ablfacrp2  15318  ablfac1a  15320  ablfac1b  15321  ablfac1c  15322  ablfac1eu  15324  pgpfaclem2  15333  ablfaclem1  15336  ablfaclem2  15337  ablfaclem3  15338  mgpplusg  15345  mgpress  15352  pwsmgp  15417  opprmulfval  15423  dvdsrval  15443  isunit  15455  unitgrp  15465  unitlinv  15475  unitrinv  15476  dvrfval  15482  isirred  15497  isdrng2  15538  drngmcl  15541  drngid2  15544  issubrg  15561  subrgugrp  15580  isabv  15600  staffval  15628  islmod  15647  scaffval  15661  lssset  15707  islss  15708  lsssn0  15721  lssacs  15740  lspfval  15746  lspval  15748  lspcl  15749  lspuni0  15783  lss0v  15789  0lmhm  15813  lmhmvsca  15818  islbs  15845  islbs3  15924  lbsextlem1  15927  lbsextlem3  15929  lbsextlem4  15930  lbsext  15932  rsp1  15992  drngnidl  15997  2idlval  16001  divsrhm  16005  isnzr2  16031  rrgval  16044  aspval  16084  asclfval  16090  gsumbagdiag  16138  psrbas  16140  psrelbas  16141  psrplusg  16142  psrmulr  16145  psrmulfval  16146  psrmulcllem  16148  psrvscafval  16151  psrvscaval  16153  psrvscacl  16154  psr0cl  16155  psr0lid  16156  psrnegcl  16157  psrlinv  16158  psr1cl  16163  psrlidm  16164  psrridm  16165  psrdi  16167  psrdir  16168  psrass23  16170  resspsradd  16176  resspsrmul  16177  resspsrvsca  16178  mvrval  16182  mvrval2  16183  mplsubglem  16195  mpladd  16202  mplmul  16203  mplvscaval  16208  ressmpladd  16217  ressmplmul  16218  ressmplvsca  16219  subrgmvr  16221  mplmon  16223  mplmonmul  16224  mplcoe1  16225  ltbval  16229  opsrle  16233  opsrtoslem2  16242  mplmon2  16250  psrbag0  16251  psrbagsn  16252  subrgascl  16255  evlslem2  16265  psr1baslem  16280  ressply1add  16324  ressply1mul  16325  ressply1vsca  16326  psropprmul  16332  coe1tmmul2fv  16370  coe1pwmulfv  16372  ply1coe  16384  xrsex  16398  expghm  16466  zrhrhmb  16481  zlmlem  16487  zlmsca  16491  zlmvsca  16492  znle  16506  znbas  16513  znzrhval  16516  zntoslem  16526  znfi  16529  znidomb  16531  znunithash  16534  ipffval  16568  ocvfval  16582  ocvval  16583  elocv  16584  thlbas  16612  thlle  16613  thlleval  16614  thloc  16615  pjfval  16622  pjdm  16623  pjpm  16624  isobs  16636  indistopon  16754  iccordt  16960  concompid  17173  ptbasfi  17292  imastopn  17427  ptcmpfi  17520  uzrest  17608  tmdgsum2  17795  distgp  17798  indistgp  17799  cldsubg  17809  snclseqg  17814  tsmsval  17829  tsmsadd  17845  prdsxmetlem  17948  tmslem  18044  nrmmetd  18113  nmfval  18127  tnglem  18172  tngds  18180  tngnm  18183  tngngp2  18184  tngngpd  18185  tngngp  18186  nghmfval  18247  nmo0  18260  cnbl0  18299  remet  18312  re2ndc  18323  xrrest  18329  zcld  18335  icccmp  18346  xrge0gsumle  18354  xrge0tsms  18355  xmetdcn  18359  divcn  18388  expcn  18392  iicon  18407  climcncf  18420  cnmpt2pc  18442  cnrehmeo  18467  cnheiborlem  18468  rellycmp  18471  bndth  18472  evth2  18474  pi1bas  18552  cphsubrglem  18629  cphcjcl  18635  tchex  18665  ipcau2  18680  cncmet  18760  cmsss  18788  ishl2  18803  minveclem4a  18810  minveclem4  18812  finiunmbl  18917  ioombl1lem4  18934  vitalilem4  18982  vitalilem5  18983  ismbf2d  19012  mbfimaopnlem  19026  mbflimsup  19037  mbflim  19039  mbfi1fseqlem6  19091  itgex  19141  bddmulibl  19209  ditgex  19218  recnperf  19271  dv11cn  19364  dvcnvrelem2  19381  ftc1  19405  evlslem3  19414  evlslem1  19415  evlsval2  19420  evl1fval  19426  evl1val  19427  evl1rhm  19428  evl1sca  19429  evl1var  19431  evl1addd  19433  evl1subd  19434  evl1muld  19435  evl1expd  19437  pf1f  19449  pf1mpf  19451  pf1ind  19454  mdegfval  19464  mdegldg  19468  mdegcl  19471  mdegmullem  19480  uc1pval  19541  mon1pval  19543  q1pval  19555  r1pval  19558  ply1remlem  19564  ply1rem  19565  facth1  19566  fta1glem1  19567  fta1glem2  19568  fta1blem  19570  ig1pval  19574  plyeq0lem  19608  quotval  19688  elqaalem3  19717  aaliou3lem4  19742  ulmcau  19788  ulmdvlem1  19793  ulmdvlem3  19795  mbfulm  19798  itgulm  19800  dvradcnv  19813  pserdvlem2  19820  sincn  19836  coscn  19837  tanabsge  19890  reloggim  19968  logcn  20010  dvloglem  20011  logdmopn  20012  dvlog2  20016  cxpcn  20101  cxpcn3  20104  resqrcn  20105  ang180lem3  20125  atanrecl  20223  atan1  20240  atansopn  20244  birthdaylem1  20262  birthday  20265  emcllem4  20308  emcllem6  20310  basellem6  20339  ppiublem1  20457  dchrplusg  20502  dchrmulid2  20507  dchrinvcl  20508  dchrptlem2  20520  dchrsum2  20523  sumdchr2  20525  dchr2sum  20528  bposlem6  20544  bposlem8  20546  lgslem4  20554  lgsdir2lem2  20579  selberglem1  20710  selberglem3  20712  selberg  20713  selbergs  20739  qdrng  20785  gxval  20941  issubgoi  20993  rngoi  21063  dvrunz  21116  isvci  21154  isnvi  21185  imsmetlem  21275  dipfval  21291  sspval  21315  islno  21347  nmooval  21357  nmounbseqi  21371  nmobndseqi  21373  bloval  21375  0ofval  21381  0oval  21382  blocni  21399  ajfval  21403  hmoval  21404  cncph  21413  isph  21416  phpar  21418  ipasslem7  21430  siilem2  21446  ajval  21456  ubthlem1  21465  ubthlem2  21466  minvecolem4b  21473  minvecolem4  21475  minvecolem5  21476  hlex  21493  normlem2  21706  normlem3  21707  normlem6  21710  h0elch  21850  hhsssh  21862  spansnji  22241  nonbooli  22246  3oalem5  22261  3oalem6  22262  3oai  22263  mayetes3i  22325  nmcexi  22622  nmbdfnlb  22646  rnelshi  22655  cnlnadjlem5  22667  pjbdlni  22745  golem2  22868  goeqi  22869  tpr2tp  23302  tpr2rico  23311  ressplusf  23313  mndpluscn  23314  xrge0pluscn  23337  xrge0mulc1cn  23338  xrge0haus  23341  lmlimxrge0  23387  pnfneige0  23389  lmxrge0  23390  xrge0tsmsd  23397  esumex  23427  esumcst  23451  hasheuni  23468  esumcvg  23469  isrnsigaOLD  23488  prsiga  23507  mbfmcnt  23588  coinflipprob  23695  subfacp1lem1  23725  subfacp1lem3  23728  subfacp1lem5  23730  subfacp1lem6  23731  kur14lem7  23758  iiscon  23798  iillyscon  23799  cvmliftlem5  23835  cvmliftlem8  23838  cvmliftlem10  23840  cvmlift2lem9  23857  eupath  23920  konigsberg  23926  ghomgrpilem2  24008  ghomsn  24010  ghomgrplem  24011  sinccvglem  24020  circum  24022  cprodex  24129  prodfclim1  24167  predasetex  24251  trpredex  24311  altopex  24566  colinearex  24755  bpoly4  24866  rankeq1o  24873  ssoninhaus  24959  areacirc  25034  fixpc  25197  domrancur1b  25303  isoriso  25315  prodex  25407  fprodp1fi  25431  fincmpzer  25453  gapm2  25472  rngounval2  25528  idlvalNEW  25548  isidlNEW  25549  mulveczer  25582  mulinvsca  25583  muldisc  25584  glmrngo  25585  svli2  25587  intopcoaconc  25644  singempcon  25696  nolimf  25722  flfnein  25724  limnumrr  25725  cinei  25726  flfneic  25727  flfneicn  25728  tcnvec  25793  intvlset  25801  dualalg  25885  dualded  25886  dualcat2  25887  ishoma  25890  ishomb  25891  ismona  25912  isepia  25922  isiso  25928  cinvlem1  25931  cinvlem2  25932  isfunb  25938  issubcat  25948  infemb  25962  smbkle  26146  fnckle  26148  pfsubkl  26150  phpf  26153  pspf  26154  pgapspf  26155  pgapspf2  26156  bisig0  26165  linevala2  26181  isibg2  26213  sgplpte21  26235  sgplpte22  26241  isray2  26256  isray  26257  pdiveql  26271  bhp3  26280  isibcg  26294  upixp  26506  sdclem2  26555  sdclem1  26556  fdc  26558  lmclim2  26577  caures  26579  idcncf  26583  cncfres  26588  heibor1lem  26636  heiborlem3  26640  heibor  26648  rrnval  26654  rrnmet  26656  reheibor  26666  grpokerinj  26678  isdrngo1  26690  isdrngo2  26692  isrngohom  26699  idlval  26741  isidl  26742  0idl  26753  0rngo  26755  divrngidl  26756  smprngopr  26780  igenval  26789  mapfzcons2  26899  jm2.23  27192  jm2.27dlem2  27206  jm2.27dlem4  27208  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  aomclem6  27259  islssfgi  27273  pwssplit4  27294  pwslnmlem0  27296  frlmbas  27326  frlmbasf  27331  frlmvscafval  27333  uvcvval  27338  uvcvvcl  27339  frlmsslss2  27348  frlmlbs  27352  ellspd  27357  elfilspd  27358  mapfien2  27361  pwfi2en  27364  frlmpwfi  27365  islinds2  27386  lsslindf  27403  lsslinds  27404  islindf4  27411  hbtlem1  27430  hbtlem7  27432  mncn0  27447  aaitgo  27470  symgfisg  27512  psgnfval  27526  cnmsgnsubg  27537  psgnghm  27540  psgnghm2  27541  mndvcl  27549  mamucl  27559  mamudiagcl  27560  mamulid  27561  mamurid  27562  mamuvs1  27566  mamuvs2  27567  matmulr  27570  mdetfval  27590  mendplusgfval  27596  mendmulrfval  27598  mendvscafval  27601  subrgacs  27611  sdrgacs  27612  cntzsdrg  27613  idomrootle  27614  idomodle  27615  deg1mhm  27629  fcnre  27799  refsumcn  27804  refsum2cnlem1  27811  clim1fr1  27830  climexp  27834  climinf  27835  climneg  27839  climdivf  27841  itgsin0pilem1  27847  stoweidlem47  27899  stoweidlem53  27905  stoweidlem57  27909  stoweidlem59  27911  wallispilem3  27919  wallispilem4  27920  wallispilem5  27921  wallispi  27922  stirlinglem1  27926  stirlinglem8  27933  stirlinglem12  27937  stirlinglem13  27938  stirlinglem14  27939  stirlinglem15  27940  usgraexmpl  28267  wlkntrl  28350  0pth  28356  eupatrl  28385  constr3lem1  28391  constr3trllem3  28398  dpval  28494  bnj105  29066  bnj918  29112  bnj95  29212  bnj852  29269  bnj865  29271  lshpset  29790  lsatset  29802  lcvfbr  29832  islfl  29872  lfl0f  29881  lfl1  29882  lfladd0l  29886  lflnegl  29888  lflvscl  29889  lflvsdi1  29890  lflvsdi2  29891  lflvsdi2a  29892  lflvsass  29893  lfl0sc  29894  lflsc0N  29895  lfl1sc  29896  lkrfval  29899  lkr0f  29906  lkrsc  29909  eqlkr2  29912  ldualvbase  29938  ldualfvadd  29940  ldualvaddval  29943  ldualsca  29944  ldualfvs  29948  ldualvsval  29950  isopos  29992  cmtfvalN  30022  cvrfval  30080  pats  30097  glbconN  30188  llnset  30316  lplnset  30340  lvolset  30383  lineset  30549  isline  30550  pointsetN  30552  psubspset  30555  ispsubsp  30556  pmapfval  30567  pmapval  30568  paddfval  30608  paddval  30609  pclfvalN  30700  pclvalN  30701  polfvalN  30715  polvalN  30716  psubclsetN  30747  ispsubclN  30748  watfvalN  30803  watvalN  30804  lhpset  30806  lautset  30893  islaut  30894  pautsetN  30909  ispautN  30910  ldilfset  30919  ldilset  30920  ltrnfset  30928  ltrnset  30929  dilfsetN  30963  dilsetN  30964  trnfsetN  30966  trlfset  30971  cdleme25cl  31168  cdleme26e  31170  cdleme26eALTN  31172  cdleme26fALTN  31173  cdleme26f  31174  cdleme26f2ALTN  31175  cdleme26f2  31176  cdleme29cl  31188  cdleme31snd  31197  cdleme31fv  31201  cdlemefrs29clN  31210  cdlemefs32sn1aw  31225  cdleme43fsv1snlem  31231  cdleme41sn3a  31244  cdleme32a  31252  cdleme40m  31278  cdleme40n  31279  cdleme42b  31289  cdlemeg46c  31324  tgrpfset  31555  tgrpbase  31557  tgrpopr  31558  tendofset  31569  istendo  31571  tendopl  31587  tendo02  31598  tendoi  31605  erngfset  31610  erngbase  31612  erngfplus  31613  erngfmul  31616  erngfset-rN  31618  erngbase-rN  31620  erngfplus-rN  31621  erngfmul-rN  31624  cdlemk29-3  31722  cdlemk36  31724  cdlemk40  31728  cdlemkid5  31746  cdlemkid  31747  cdlemk56  31782  dvafset  31815  dvasca  31817  dvavbase  31824  dvafvadd  31825  dvafvsca  31827  diaffval  31842  diafval  31843  diaval  31844  dvhfset  31892  dvhsca  31894  dvhvbase  31899  dvhfvadd  31903  dvhfvsca  31912  docaffvalN  31933  docafvalN  31934  docavalN  31935  djaffvalN  31945  djafvalN  31946  djavalN  31947  dibffval  31952  dibfval  31953  dibopelvalN  31955  dibopelval2  31957  dibelval3  31959  diblsmopel  31983  dicffval  31986  dicfval  31987  dicval  31988  cdlemn11a  32019  dihffval  32042  dihfval  32043  dihvalcqpre  32047  dihopelvalcpre  32060  dihord6apre  32068  dihpN  32148  dochffval  32161  dochfval  32162  dochval  32163  djhffval  32208  djhfval  32209  djhval  32210  islpolN  32295  lpolconN  32299  dochpolN  32302  lcfrlem8  32361  lcfrlem9  32362  lcdfval  32400  lcd0vvalN  32425  mapdffval  32438  mapdfval  32439  mapdval  32440  mapd1o  32460  mapdunirnN  32462  mapdhval  32536  mapdhval0  32537  hvmapffval  32570  hvmapfval  32571  hvmapval  32572  hdmap1ffval  32608  hdmap1fval  32609  hdmap1vallem  32610  hdmapffval  32641  hdmapfval  32642  hgmapffval  32700  hgmapfval  32701  hlhilset  32749  hlhilsca  32750  hlhilbase  32751  hlhilplus  32752  hlhilvsca  32762  hlhilip  32763  hlhilnvl  32765  hlhillsm  32771  hlhillcs  32773
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-ex 1532  df-cleq 2289  df-clel 2292
  Copyright terms: Public domain W3C validator