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

Theorem 3eltr4d 2745
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 2733 . 2 (𝜑𝐴𝐷)
51, 4eqeltrd 2730 1 (𝜑𝐶𝐷)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  elimdelov  6778  ovmpt2dxf  6828  cantnflt  8607  cantnflem1  8624  cofsmo  9129  cfsmolem  9130  axcclem  9317  smobeth  9446  iccf1o  12354  ccatw2s1p1  13458  revccat  13561  pwp1fsum  15161  vdwlem8  15739  issubc3  16556  cofucl  16595  catccatid  16799  xpccatid  16875  issstrmgm  17299  mndpropd  17363  issubmnd  17365  pwspjmhm  17415  gsumccat  17425  imasgrp  17578  mulgnndir  17616  mulgnndirOLD  17617  subg0cl  17649  subginvcl  17650  subgcl  17651  psgnunilem2  17961  efgsp1  18196  gsumzsubmcl  18364  dpjghm  18508  pwsco1rhm  18786  pwsco2rhm  18787  isdrngd  18820  subrgmcl  18840  subrgunit  18846  issubdrg  18853  lmodprop2d  18973  psraddcl  19431  psrmulcllem  19435  psrvscacl  19441  qsssubdrg  19853  matgsum  20291  mat1rhmcl  20335  dmatmulcl  20354  scmatghm  20387  imacmp  21248  prdstps  21480  symgtgp  21952  tsmssub  21999  ustuqtop3  22094  utop2nei  22101  xpsxmetlem  22231  xpsmet  22234  imasf1oxms  22341  imasf1oms  22342  prdsmslem1  22379  prdsxmslem1  22380  prdsxmslem2  22381  tngngp2  22503  cnmpt2pc  22774  caublcls  23153  minveclem3a  23244  efsubm  24342  wlkl1loop  26590  clwwlknonex2lem1  27082  eucrct2eupth  27223  cvmliftlem7  31399  cvmliftlem10  31402  prdsbnd  33722  prdstotbnd  33723  prdsbnd2  33724  cnpwstotbnd  33726  repwsmet  33763  diblss  36776  kelac1  37950  iunrelexpuztr  38328  fnchoice  39502  sumnnodd  40180  sublimc  40202  divlimc  40206  cncfshiftioo  40423  itgperiod  40515  stoweidlem26  40561  dirkercncflem2  40639  fourierdlem32  40674  fourierdlem33  40675  fourierdlem46  40687  fourierdlem48  40689  fourierdlem49  40690  fourierdlem62  40703  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem81  40722  fourierdlem88  40729  fourierdlem89  40730  fourierdlem91  40732  fourierdlem93  40734  fourierdlem103  40744  fourierdlem104  40745  fouriersw  40766  fouriercn  40767  uspgropssxp  42077  issubmgm2  42115  rnghmsubcsetclem1  42300  rnghmsubcsetclem2  42301  rngccatidALTV  42314  funcrngcsetc  42323  rhmsubcsetclem1  42346  rhmsubcsetclem2  42347  rhmsubcrngclem1  42352  rhmsubcrngclem2  42353  funcringcsetc  42360  ringccatidALTV  42377  srhmsubc  42401  rhmsubclem3  42413  rhmsubclem4  42414  srhmsubcALTV  42419  rhmsubcALTVlem3  42431  rhmsubcALTVlem4  42432  ovmpt2rdxf  42442
  Copyright terms: Public domain W3C validator