Theorem 3eltr4d 2703

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

Step	Hyp	Ref	Expression
1		3eltr4d.2	. 2 ⊢ (𝜑 → 𝐶 = 𝐴)
2		3eltr4d.1	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝐵)
3		3eltr4d.3	. . 3 ⊢ (𝜑 → 𝐷 = 𝐵)
4	2, 3	eleqtrrd 2691	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐷)
5	1, 4	eqeltrd 2688	1 ⊢ (𝜑 → 𝐶 ∈ 𝐷)

Syntax hints:   → wi 4   = wceq 1475   ∈ wcel 1977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-an 385  df-ex 1696  df-cleq 2603  df-clel 2606

This theorem is referenced by:  elimdelov  6634  ovmpt2dxf  6684  cantnflt  8452  cantnflem1  8469  cofsmo  8974  cfsmolem  8975  axcclem  9162  smobeth  9287  iccf1o  12187  ccatw2s1p1  13265  revccat  13366  pwp1fsum  14952  vdwlem8  15530  issubc3  16332  cofucl  16371  catccatid  16575  xpccatid  16651  issstrmgm  17075  mndpropd  17139  issubmnd  17141  pwspjmhm  17191  gsumccat  17201  imasgrp  17354  mulgnndir  17392  mulgnndirOLD  17393  subg0cl  17425  subginvcl  17426  subgcl  17427  psgnunilem2  17738  efgsp1  17973  gsumzsubmcl  18141  dpjghm  18285  pwsco1rhm  18561  pwsco2rhm  18562  isdrngd  18595  subrgmcl  18615  subrgunit  18621  issubdrg  18628  lmodprop2d  18748  psraddcl  19204  psrmulcllem  19208  psrvscacl  19214  qsssubdrg  19624  matgsum  20062  mat1rhmcl  20106  dmatmulcl  20125  scmatghm  20158  imacmp  21010  prdstps  21242  symgtgp  21715  tsmssub  21762  ustuqtop3  21857  utop2nei  21864  xpsxmetlem  21994  xpsmet  21997  imasf1oxms  22104  imasf1oms  22105  prdsmslem1  22142  prdsxmslem1  22143  prdsxmslem2  22144  tngngp2  22266  cnmpt2pc  22535  caublcls  22915  minveclem3a  23006  efsubm  24101  cvmliftlem7  30527  cvmliftlem10  30530  prdsbnd  32762  prdstotbnd  32763  prdsbnd2  32764  cnpwstotbnd  32766  repwsmet  32803  diblss  35477  kelac1  36651  iunrelexpuztr  37030  fnchoice  38211  sumnnodd  38697  sublimc  38719  divlimc  38723  cncfshiftioo  38778  itgperiod  38873  stoweidlem26  38919  dirkercncflem2  38997  fourierdlem32  39032  fourierdlem33  39033  fourierdlem46  39045  fourierdlem48  39047  fourierdlem49  39048  fourierdlem62  39061  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem81  39080  fourierdlem88  39087  fourierdlem89  39088  fourierdlem91  39090  fourierdlem93  39092  fourierdlem103  39102  fourierdlem104  39103  fouriersw  39124  fouriercn  39125  1wlkl1loop  40842  eucrct2eupth  41413  issubmgm2  41580  rnghmsubcsetclem1  41767  rnghmsubcsetclem2  41768  rngccatidALTV  41781  funcrngcsetc  41790  rhmsubcsetclem1  41813  rhmsubcsetclem2  41814  rhmsubcrngclem1  41819  rhmsubcrngclem2  41820  funcringcsetc  41827  ringccatidALTV  41844  srhmsubc  41868  rhmsubclem3  41880  rhmsubclem4  41881  srhmsubcALTV  41887  rhmsubcALTVlem3  41899  rhmsubcALTVlem4  41900  ovmpt2rdxf  41910