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

Theorem 3eltr4d 2842
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 2830 . 2 (𝜑𝐴𝐷)
51, 4eqeltrd 2827 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1620  wcel 2127
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1842  df-cleq 2741  df-clel 2744
This theorem is referenced by:  elimdelov  6889  ovmpt2dxf  6939  cantnflt  8730  cantnflem1  8747  cofsmo  9254  cfsmolem  9255  axcclem  9442  smobeth  9571  iccf1o  12480  ccatw2s1p1  13583  revccat  13686  pwp1fsum  15287  vdwlem8  15865  issubc3  16681  cofucl  16720  catccatid  16924  xpccatid  17000  issstrmgm  17424  mndpropd  17488  issubmnd  17490  pwspjmhm  17540  gsumccat  17550  imasgrp  17703  mulgnndir  17741  mulgnndirOLD  17742  subg0cl  17774  subginvcl  17775  subgcl  17776  psgnunilem2  18086  efgsp1  18321  gsumzsubmcl  18489  dpjghm  18633  pwsco1rhm  18911  pwsco2rhm  18912  isdrngd  18945  subrgmcl  18965  subrgunit  18971  issubdrg  18978  lmodprop2d  19098  psraddcl  19556  psrmulcllem  19560  psrvscacl  19566  qsssubdrg  19978  matgsum  20416  mat1rhmcl  20460  dmatmulcl  20479  scmatghm  20512  imacmp  21373  prdstps  21605  symgtgp  22077  tsmssub  22124  ustuqtop3  22219  utop2nei  22226  xpsxmetlem  22356  xpsmet  22359  imasf1oxms  22466  imasf1oms  22467  prdsmslem1  22504  prdsxmslem1  22505  prdsxmslem2  22506  tngngp2  22628  cnmpt2pc  22899  caublcls  23278  minveclem3a  23369  efsubm  24467  wlkl1loop  26715  clwwlknonex2lem1  27227  eucrct2eupth  27368  cvmliftlem7  31551  cvmliftlem10  31554  prdsbnd  33874  prdstotbnd  33875  prdsbnd2  33876  cnpwstotbnd  33878  repwsmet  33915  diblss  36930  kelac1  38104  iunrelexpuztr  38482  fnchoice  39656  sumnnodd  40334  sublimc  40356  divlimc  40360  cncfshiftioo  40577  itgperiod  40669  stoweidlem26  40715  dirkercncflem2  40793  fourierdlem32  40828  fourierdlem33  40829  fourierdlem46  40841  fourierdlem48  40843  fourierdlem49  40844  fourierdlem62  40857  fourierdlem74  40869  fourierdlem75  40870  fourierdlem76  40871  fourierdlem81  40876  fourierdlem88  40883  fourierdlem89  40884  fourierdlem91  40886  fourierdlem93  40888  fourierdlem103  40898  fourierdlem104  40899  fouriersw  40920  fouriercn  40921  uspgropssxp  42231  issubmgm2  42269  rnghmsubcsetclem1  42454  rnghmsubcsetclem2  42455  rngccatidALTV  42468  funcrngcsetc  42477  rhmsubcsetclem1  42500  rhmsubcsetclem2  42501  rhmsubcrngclem1  42506  rhmsubcrngclem2  42507  funcringcsetc  42514  ringccatidALTV  42531  srhmsubc  42555  rhmsubclem3  42567  rhmsubclem4  42568  srhmsubcALTV  42573  rhmsubcALTVlem3  42585  rhmsubcALTVlem4  42586  ovmpt2rdxf  42596
  Copyright terms: Public domain W3C validator