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

Theorem 3eltr4d 2713
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 2701 . 2 (𝜑𝐴𝐷)
51, 4eqeltrd 2698 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wcel 1987
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1702  df-cleq 2614  df-clel 2617
This theorem is referenced by:  elimdelov  6689  ovmpt2dxf  6739  cantnflt  8513  cantnflem1  8530  cofsmo  9035  cfsmolem  9036  axcclem  9223  smobeth  9352  iccf1o  12258  ccatw2s1p1  13351  revccat  13452  pwp1fsum  15038  vdwlem8  15616  issubc3  16430  cofucl  16469  catccatid  16673  xpccatid  16749  issstrmgm  17173  mndpropd  17237  issubmnd  17239  pwspjmhm  17289  gsumccat  17299  imasgrp  17452  mulgnndir  17490  mulgnndirOLD  17491  subg0cl  17523  subginvcl  17524  subgcl  17525  psgnunilem2  17836  efgsp1  18071  gsumzsubmcl  18239  dpjghm  18383  pwsco1rhm  18659  pwsco2rhm  18660  isdrngd  18693  subrgmcl  18713  subrgunit  18719  issubdrg  18726  lmodprop2d  18846  psraddcl  19302  psrmulcllem  19306  psrvscacl  19312  qsssubdrg  19724  matgsum  20162  mat1rhmcl  20206  dmatmulcl  20225  scmatghm  20258  imacmp  21110  prdstps  21342  symgtgp  21815  tsmssub  21862  ustuqtop3  21957  utop2nei  21964  xpsxmetlem  22094  xpsmet  22097  imasf1oxms  22204  imasf1oms  22205  prdsmslem1  22242  prdsxmslem1  22243  prdsxmslem2  22244  tngngp2  22366  cnmpt2pc  22635  caublcls  23015  minveclem3a  23106  efsubm  24201  wlkl1loop  26403  eucrct2eupth  26971  cvmliftlem7  30978  cvmliftlem10  30981  prdsbnd  33221  prdstotbnd  33222  prdsbnd2  33223  cnpwstotbnd  33225  repwsmet  33262  diblss  35936  kelac1  37110  iunrelexpuztr  37489  fnchoice  38668  sumnnodd  39263  sublimc  39285  divlimc  39289  cncfshiftioo  39406  itgperiod  39501  stoweidlem26  39547  dirkercncflem2  39625  fourierdlem32  39660  fourierdlem33  39661  fourierdlem46  39673  fourierdlem48  39675  fourierdlem49  39676  fourierdlem62  39689  fourierdlem74  39701  fourierdlem75  39702  fourierdlem76  39703  fourierdlem81  39708  fourierdlem88  39715  fourierdlem89  39716  fourierdlem91  39718  fourierdlem93  39720  fourierdlem103  39730  fourierdlem104  39731  fouriersw  39752  fouriercn  39753  uspgropssxp  41037  issubmgm2  41075  rnghmsubcsetclem1  41260  rnghmsubcsetclem2  41261  rngccatidALTV  41274  funcrngcsetc  41283  rhmsubcsetclem1  41306  rhmsubcsetclem2  41307  rhmsubcrngclem1  41312  rhmsubcrngclem2  41313  funcringcsetc  41320  ringccatidALTV  41337  srhmsubc  41361  rhmsubclem3  41373  rhmsubclem4  41374  srhmsubcALTV  41379  rhmsubcALTVlem3  41391  rhmsubcALTVlem4  41392  ovmpt2rdxf  41402
  Copyright terms: Public domain W3C validator