Theorem eqeltri 2243

Description: Substitution of equal classes into membership relation. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
eqeltr.1	⊢ 𝐴 = 𝐵
eqeltr.2	⊢ 𝐵 ∈ 𝐶

Assertion

Ref	Expression
eqeltri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eqeltri

Step	Hyp	Ref	Expression
1		eqeltr.2	. 2 ⊢ 𝐵 ∈ 𝐶
2		eqeltr.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	eleq1i 2236	. 2 ⊢ (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)
4	1, 3	mpbir 145	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1348   ∈ wcel 2141

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1440  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-cleq 2163  df-clel 2166

This theorem is referenced by:  eqeltrri  2244  3eltr4i  2252  intab  3860  inex2  4124  vpwex  4165  ord3ex  4176  uniopel  4241  onsucelsucexmid  4514  nnpredcl  4607  elvvuni  4675  isarep2  5285  acexmidlemcase  5848  abrexex2  6103  oprabex  6107  oprabrexex2  6109  mpoexw  6192  rdg0  6366  frecex  6373  1on  6402  2on  6404  3on  6406  4on  6407  1onn  6499  2onn  6500  3onn  6501  4onn  6502  mapsnf1o2  6674  exmidpw  6886  unfiexmid  6895  xpfi  6907  ssfirab  6911  fnfi  6914  iunfidisj  6923  fidcenumlemr  6932  sbthlemi10  6943  ctmlemr  7085  nninfex  7098  exmidonfinlem  7170  acfun  7184  exmidaclem  7185  pw1ne1  7206  ccfunen  7226  nqex  7325  nq0ex  7402  1pr  7516  ltexprlempr  7570  recexprlempr  7594  cauappcvgprlemcl  7615  caucvgprlemcl  7638  caucvgprprlemcl  7666  addvalex  7806  peano1nnnn  7814  peano2nnnn  7815  axcnex  7821  ax1cn  7823  ax1re  7824  pnfxr  7972  mnfxr  7976  inelr  8503  cju  8877  2re  8948  3re  8952  4re  8955  5re  8957  6re  8959  7re  8961  8re  8963  9re  8965  2nn  9039  3nn  9040  4nn  9041  5nn  9042  6nn  9043  7nn  9044  8nn  9045  9nn  9046  nn0ex  9141  nneoor  9314  zeo  9317  deccl  9357  decnncl  9362  numnncl2  9365  decnncl2  9366  numsucc  9382  numma2c  9388  numadd  9389  numaddc  9390  nummul1c  9391  nummul2c  9392  xnegcl  9789  xrex  9813  ioof  9928  uzennn  10392  seqex  10403  m1expcl2  10498  faccl  10669  facwordi  10674  faclbnd2  10676  bccl  10701  crre  10821  remim  10824  absval  10965  climle  11297  climcvg1nlem  11312  iserabs  11438  geo2lim  11479  prodfclim1  11507  fprodle  11603  ere  11633  ege2le3  11634  eftlub  11653  efsep  11654  tan0  11694  ef01bndlem  11719  nn0o  11866  pczpre  12251  pockthi  12310  igz  12326  ennnfonelemj0  12356  ennnfonelem0  12360  ndxarg  12439  ndxslid  12441  strndxid  12444  basendxnn  12471  strle1g  12508  2strbasg  12519  2stropg  12520  setsmsbasg  13273  cnbl0  13328  cnopncntop  13331  remet  13334  divcnap  13349  climcncf  13365  expcncf  13386  cnrehmeocntop  13387  sincn  13484  coscn  13485  2logb9irrALT  13686  2irrexpq  13688  2irrexpqap  13690  lgslem4  13698  lgsdir2lem2  13724  bdinex2  13935  bj-inex  13942  012of  14028  2o01f  14029  peano3nninf  14040  cvgcmp2nlemabs  14064  trilpolemisumle  14070