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

Theorem 3eltr4d 2925
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 2913 . 2 (𝜑𝐴𝐷)
51, 4eqeltrd 2910 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  wcel 2105
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-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811  df-clel 2890
This theorem is referenced by:  elimdelov  7239  ovmpodxf  7289  cantnflt  9123  cantnflem1  9140  cofsmo  9679  cfsmolem  9680  axcclem  9867  smobeth  9996  iccf1o  12870  ccatw2s1p1  13983  ccatw2s1p1OLD  13984  revccat  14116  pwp1fsum  15730  vdwlem8  16312  issubc3  17107  cofucl  17146  catccatid  17350  xpccatid  17426  issstrmgm  17851  mndpropd  17924  issubmnd  17926  pwspjmhm  17982  gsumsgrpccat  17992  gsumccatOLD  17993  pwmnd  18040  imasgrp  18153  mulgnndir  18194  subg0cl  18225  subginvcl  18226  subgcl  18227  psgnunilem2  18552  efgsp1  18792  gsumzsubmcl  18967  dpjghm  19114  pwsco1rhm  19419  pwsco2rhm  19420  isdrngd  19456  subrgmcl  19476  subrgunit  19482  issubdrg  19489  lmodprop2d  19625  psraddcl  20091  psrmulcllem  20095  psrvscacl  20101  qsssubdrg  20532  matgsum  20974  mat1rhmcl  21018  dmatmulcl  21037  scmatghm  21070  imacmp  21933  prdstps  22165  symgtgp  22637  prdstgpd  22660  tsmssub  22684  ustuqtop3  22779  utop2nei  22786  xpsxmetlem  22916  xpsmet  22919  imasf1oxms  23026  imasf1oms  23027  prdsmslem1  23064  prdsxmslem1  23065  prdsxmslem2  23066  tngngp2  23188  cnmpopc  23459  caublcls  23839  minveclem3a  23957  efsubm  25062  wlkl1loop  27346  wlkres  27379  clwwlknonex2lem1  27813  eucrct2eupth  27951  cyc3co2  30709  drgextlsp  30895  fedgmullem2  30925  cvmliftlem7  32435  cvmliftlem10  32438  ex-sategoelel  32565  ex-sategoelelomsuc  32570  prdsbnd  34952  prdstotbnd  34953  prdsbnd2  34954  cnpwstotbnd  34956  repwsmet  34993  diblss  38186  kelac1  39541  iunrelexpuztr  39942  mnuprdlem3  40487  fnchoice  41163  sumnnodd  41787  sublimc  41809  divlimc  41813  cncfshiftioo  42051  itgperiod  42142  stoweidlem26  42188  dirkercncflem2  42266  fourierdlem32  42301  fourierdlem33  42302  fourierdlem46  42314  fourierdlem48  42316  fourierdlem49  42317  fourierdlem62  42330  fourierdlem74  42342  fourierdlem75  42343  fourierdlem76  42344  fourierdlem81  42349  fourierdlem88  42356  fourierdlem89  42357  fourierdlem91  42359  fourierdlem93  42361  fourierdlem103  42371  fourierdlem104  42372  fouriersw  42393  fouriercn  42394  uspgropssxp  43896  issubmgm2  43934  smndex1gbas  44002  rnghmsubcsetclem1  44174  rnghmsubcsetclem2  44175  rngccatidALTV  44188  funcrngcsetc  44197  rhmsubcsetclem1  44220  rhmsubcsetclem2  44221  rhmsubcrngclem1  44226  rhmsubcrngclem2  44227  funcringcsetc  44234  ringccatidALTV  44251  srhmsubc  44275  rhmsubclem3  44287  rhmsubclem4  44288  srhmsubcALTV  44293  rhmsubcALTVlem3  44305  rhmsubcALTVlem4  44306  ovmpordxf  44315
  Copyright terms: Public domain W3C validator