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

Theorem 3eltr4d 2908
Description: Substitution of equal classes into membership relation. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
3eltr4d.1 (𝜑𝐴𝐵)
3eltr4d.2 (𝜑𝐶 = 𝐴)
3eltr4d.3 (𝜑𝐷 = 𝐵)
Assertion
Ref Expression
3eltr4d (𝜑𝐶𝐷)

Proof of Theorem 3eltr4d
StepHypRef Expression
1 3eltr4d.2 . 2 (𝜑𝐶 = 𝐴)
2 3eltr4d.1 . . 3 (𝜑𝐴𝐵)
3 3eltr4d.3 . . 3 (𝜑𝐷 = 𝐵)
42, 3eleqtrrd 2896 . 2 (𝜑𝐴𝐷)
51, 4eqeltrd 2893 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  wcel 2112
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 1911  ax-6 1970  ax-7 2015  ax-8 2114  ax-9 2122  ax-ext 2773
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2794  df-clel 2873
This theorem is referenced by:  elimdelov  7233  ovmpodxf  7283  cantnflt  9123  cantnflem1  9140  cofsmo  9684  cfsmolem  9685  axcclem  9872  smobeth  10001  iccf1o  12878  ccatw2s1p1  13990  ccatw2s1p1OLD  13991  revccat  14123  pwp1fsum  15736  vdwlem8  16318  issubc3  17115  cofucl  17154  catccatid  17358  xpccatid  17434  issstrmgm  17859  mndpropd  17932  issubmnd  17934  pwspjmhm  17990  gsumsgrpccat  18000  gsumccatOLD  18001  smndex1gbas  18063  pwmnd  18098  imasgrp  18211  mulgnndir  18252  subg0cl  18283  subginvcl  18284  subgcl  18285  psgnunilem2  18619  efgsp1  18859  gsumzsubmcl  19035  dpjghm  19182  pwsco1rhm  19490  pwsco2rhm  19491  isdrngd  19524  subrgmcl  19544  subrgunit  19550  issubdrg  19557  lmodprop2d  19693  qsssubdrg  20154  psraddcl  20625  psrmulcllem  20629  psrvscacl  20635  matgsum  21046  mat1rhmcl  21090  dmatmulcl  21109  scmatghm  21142  imacmp  22006  prdstps  22238  symgtgp  22715  prdstgpd  22734  tsmssub  22758  ustuqtop3  22853  utop2nei  22860  xpsxmetlem  22990  xpsmet  22993  imasf1oxms  23100  imasf1oms  23101  prdsmslem1  23138  prdsxmslem1  23139  prdsxmslem2  23140  tngngp2  23262  cnmpopc  23537  caublcls  23917  minveclem3a  24035  efsubm  25147  wlkl1loop  27431  wlkres  27464  clwwlknonex2lem1  27896  eucrct2eupth  28034  cyc3co2  30836  drgextlsp  31088  fedgmullem2  31118  cvmliftlem7  32652  cvmliftlem10  32655  ex-sategoelel  32782  ex-sategoelelomsuc  32787  prdsbnd  35230  prdstotbnd  35231  prdsbnd2  35232  cnpwstotbnd  35234  repwsmet  35271  diblss  38465  kelac1  40004  iunrelexpuztr  40417  mnuprdlem3  40979  fnchoice  41655  sumnnodd  42269  sublimc  42291  divlimc  42295  cncfshiftioo  42531  itgperiod  42620  stoweidlem26  42665  dirkercncflem2  42743  fourierdlem32  42778  fourierdlem33  42779  fourierdlem46  42791  fourierdlem48  42793  fourierdlem49  42794  fourierdlem62  42807  fourierdlem74  42819  fourierdlem75  42820  fourierdlem76  42821  fourierdlem81  42826  fourierdlem88  42833  fourierdlem89  42834  fourierdlem91  42836  fourierdlem93  42838  fourierdlem103  42848  fourierdlem104  42849  fouriersw  42870  fouriercn  42871  uspgropssxp  44369  issubmgm2  44407  rnghmsubcsetclem1  44596  rnghmsubcsetclem2  44597  rngccatidALTV  44610  funcrngcsetc  44619  rhmsubcsetclem1  44642  rhmsubcsetclem2  44643  rhmsubcrngclem1  44648  rhmsubcrngclem2  44649  funcringcsetc  44656  ringccatidALTV  44673  srhmsubc  44697  rhmsubclem3  44709  rhmsubclem4  44710  srhmsubcALTV  44715  rhmsubcALTVlem3  44727  rhmsubcALTVlem4  44728  ovmpordxf  44737
  Copyright terms: Public domain W3C validator