Theorem eqeltrrd 2192

Description: Deduction that substitutes equal classes into membership. (Contributed by NM, 14-Dec-2004.)

Hypotheses

Ref	Expression
eqeltrrd.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqeltrrd.2	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Assertion

Ref	Expression
eqeltrrd	⊢ (𝜑 → 𝐵 ∈ 𝐶)

Proof of Theorem eqeltrrd

Step	Hyp	Ref	Expression
1		eqeltrrd.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2	1	eqcomd 2120	. 2 ⊢ (𝜑 → 𝐵 = 𝐴)
3		eqeltrrd.2	. 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶)
4	2, 3	eqeltrd 2191	1 ⊢ (𝜑 → 𝐵 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1314   ∈ wcel 1463

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-4 1470  ax-17 1489  ax-ial 1497  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-cleq 2108  df-clel 2111

This theorem is referenced by:  3eltr3d  2197  exmid01  4081  pwntru  4082  xpexr2m  4938  funimaexg  5165  fvmptdv2  5464  ffvresb  5537  2ndrn  6035  1st2ndbr  6036  elopabi  6047  cnvf1olem  6075  dftpos4  6114  tfrlemibxssdm  6178  tfr1onlembxssdm  6194  tfrcllembxssdm  6207  nnmordi  6366  th3qlem1  6485  infiexmid  6724  onunsnss  6758  ssfirab  6774  ssfidc  6775  fnfi  6777  fidcenumlemr  6795  elfi2  6812  ordiso2  6872  djulclb  6892  ctmlemr  6945  ctssdccl  6948  ctssdc  6950  exmidfodomrlemreseldju  7004  exmidfodomrlemr  7006  archnqq  7173  prarloclemarch2  7175  enq0tr  7190  nqnq0  7197  addcmpblnq0  7199  mulcmpblnq0  7200  mulcanenq0ec  7201  addclnq0  7207  mulclnq0  7208  nqpnq0nq  7209  nq0m0r  7212  distrnq0  7215  addassnq0lemcl  7217  prarloclemlt  7249  prarloclem5  7256  distrlem4prl  7340  distrlem4pru  7341  ltexprlemm  7356  ltexprlemrl  7366  ltexprlemru  7368  addcanprleml  7370  cauappcvgprlemladdru  7412  prsrlem1  7485  mulgt0sr  7520  cnegexlem2  7861  subf  7887  resubcl  7949  negcon1ad  7991  subeq0bd  8060  rimul  8265  rereim  8266  nn0nnaddcl  8912  elnn0nn  8923  zaddcllemneg  8997  zsubcl  8999  zrevaddcl  9008  elz2  9026  zdiv  9043  peano5uzti  9063  peano2uzr  9282  uzaddcl  9283  divfnzn  9315  qsubcl  9332  qrevaddcl  9338  fseq1p1m1  9767  modqmuladdim  10033  frec2uzrand  10071  frecuzrdglem  10077  frecuzrdg0  10079  frecuzrdgdomlem  10083  frecuzrdg0t  10088  frecuzrdgsuctlem  10089  seq3val  10124  seq3feq  10138  iseqf1olemnab  10154  seqfeq3  10178  expaddzaplem  10229  expaddzap  10230  expmulzap  10232  zesq  10303  bcm1k  10399  bccl  10406  permnn  10410  seq3coll  10478  shftuz  10482  ref  10520  imf  10521  crre  10522  rereb  10528  resqrexlemnm  10682  absf  10774  summodclem2a  11042  summodc  11044  fsumgcl  11047  fsum3  11048  fsumf1o  11051  fsumcnv  11098  mptfzshft  11103  isumlessdc  11157  geolim2  11173  oexpneg  11422  nn0ob  11453  divalglemqt  11464  gcdf  11509  lcmgcdlem  11604  sqnprm  11662  sqrt2irrlem  11685  2sqpwodd  11699  fnum  11713  fden  11714  phimullem  11746  ctiunctlemfo  11795  unopn  12015  tsettps  12048  tgss2  12091  difopn  12120  resttop  12182  resttopon  12183  restco  12186  tgcn  12219  tgcnp  12220  cnptopco  12233  upxp  12283  txcn  12286  txdis  12288  cnmpt11  12294  cnmpt11f  12295  cnmpt1t  12296  cnmpt12  12298  cnmpt21  12302  cnmpt21f  12303  cnmpt2t  12304  cnmpt22  12305  cnmpt22f  12306  cnmpt1res  12307  xmeter  12425  mscl  12454  xmscl  12455  bdxmet  12490  cncfmpt1f  12570  cdivcncfap  12573  negfcncf  12575  cnmptlimc  12599  dvcnp2cntop  12618  pwtrufal  12882