Theorem 3eltr4d 2560

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 2548	. 2
5	1, 4	eqeltrd 2545	1

Syntax hints:  ->wi 4  =wceq 1395  e.wcel 1818

This theorem is referenced by:  elimdelov  6378  ovmpt2dxf  6428  cantnflt  8112  cantnflem1  8129  cantnfltOLD  8142  cofsmo  8670  cfsmolem  8671  axcclem  8858  smobeth  8982  iccf1o  11693  revccat  12740  vdwlem8  14506  issubc3  15218  cofucl  15257  catccatid  15429  xpccatid  15457  mndpropd  15946  issubmnd  15948  pwspjmhm  15999  gsumccat  16009  mulgnndir  16164  imasgrp  16186  subg0cl  16209  subginvcl  16210  subgcl  16211  psgnunilem2  16520  efgsp1  16755  gsumzsubmcl  16928  gsumzsubmclOLD  16929  dpjghm  17112  pwsco1rhm  17387  pwsco2rhm  17388  isdrngd  17421  subrgmcl  17441  subrgunit  17447  issubdrg  17454  lmodprop2d  17572  psraddcl  18036  psrmulcllem  18040  psrvscacl  18046  qsssubdrg  18477  matgsum  18939  mat1rhmcl  18983  dmatmulcl  19002  scmatghm  19035  imacmp  19897  prdstps  20130  symgtgp  20600  tsmssub  20651  ustuqtop3  20746  utop2nei  20753  xpsxmetlem  20882  xpsmet  20885  imasf1oxms  20992  imasf1oms  20993  prdsmslem1  21030  prdsxmslem1  21031  prdsxmslem2  21032  tngngp2  21166  cnmpt2pc  21428  caublcls  21747  minveclem3a  21842  efsubm  22938  cvmliftlem7  28736  cvmliftlem10  28739  prdsbnd  30289  prdstotbnd  30290  prdsbnd2  30291  cnpwstotbnd  30293  repwsmet  30330  kelac1  31009  fnchoice  31404  sumnnodd  31636  sublimc  31658  divlimc  31662  cncfshiftioo  31695  itgperiod  31780  stoweidlem26  31808  dirkercncflem2  31886  fourierdlem32  31921  fourierdlem33  31922  fourierdlem46  31935  fourierdlem48  31937  fourierdlem49  31938  fourierdlem62  31951  fourierdlem74  31963  fourierdlem75  31964  fourierdlem76  31965  fourierdlem81  31970  fourierdlem88  31977  fourierdlem89  31978  fourierdlem91  31980  fourierdlem93  31982  fourierdlem103  31992  fourierdlem104  31993  fouriersw  32014  fouriercn  32015  issubmgm2  32478  rnghmsubcsetclem1  32783  rnghmsubcsetclem2  32784  rngccatidOLD  32797  funcrngcsetc  32806  rhmsubcsetclem1  32829  rhmsubcsetclem2  32830  rhmsubcrngclem1  32835  rhmsubcrngclem2  32836  funcringcsetc  32843  ringccatidOLD  32860  srhmsubc  32884  rhmsubclem3  32896  rhmsubclem4  32897  srhmsubcOLD  32903  rhmsubcOLDlem3  32915  rhmsubcOLDlem4  32916  ovmpt2rdxf  32928  diblss  36897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1613  df-cleq 2449  df-clel 2452