Theorem eqeltrrdi 2837

Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)

Hypotheses

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

Assertion

Ref	Expression
eqeltrrdi	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrdi

Step	Hyp	Ref	Expression
1		eqeltrrdi.1	. . 3 ⊢ (𝜑 → 𝐵 = 𝐴)
2	1	eqcomd 2735	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
3		eqeltrrdi.2	. 2 ⊢ 𝐵 ∈ 𝐶
4	2, 3	eqeltrdi 2836	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-clel 2803

This theorem is referenced by:  axrep6g  5245  snexg  5390  wemoiso2  7953  releldm2  8022  mapprc  8803  mapfoss  8825  ixpprc  8892  bren  8928  brdomg  8930  domssex  9102  mapen  9105  ssenen  9115  imafiOLD  9265  fodomfib  9280  fodomfibOLD  9282  fi0  9371  dffi3  9382  brwdom  9520  brwdomn0  9522  unxpwdom2  9541  ixpiunwdom  9543  tcmin  9694  rankonid  9782  rankr1id  9815  cardf2  9896  cardid2  9906  carduni  9934  fseqen  9980  acndom  10004  acndom2  10007  alephnbtwn  10024  cardcf  10205  cfeq0  10209  cflim2  10216  coftr  10226  infpssr  10261  hsmexlem5  10383  axdc3lem4  10406  fodomb  10479  ondomon  10516  gruina  10771  ioof  13408  hashbc  14418  trclun  14980  zsum  15684  fsum  15686  fprod  15907  eqgen  19113  symgfisg  19398  dvdsr  20271  asplss  21783  aspsubrg  21785  psrval  21824  clsf  22935  restco  23051  subbascn  23141  is2ndc  23333  ptbasin2  23465  ptbas  23466  indishmph  23685  ufldom  23849  cnextfres1  23955  ussid  24148  icopnfcld  24655  cnrehmeo  24851  cnrehmeoOLD  24852  csscld  25149  clsocv  25150  itg2gt0  25661  dvmptadd  25864  dvmptmul  25865  dvmptco  25876  logcn  26556  selberglem1  27456  noseq0  28184  hmopidmchi  32080  evl1deg2  33546  sigagensiga  34131  dya2iocbrsiga  34266  dya2icobrsiga  34267  logdivsqrle  34641  fnessref  36345  bj-snexg  37022  bj-unexg  37026  unirep  37708  indexdom  37728  dicfnN  41177  pwslnmlem0  43080  mendval  43168  orbitinit  44946  icof  45213  dvsubf  45912  dvdivf  45920  itgsinexplem1  45952  stirlinglem7  46078  fourierdlem73  46177  fouriersw  46229  ovolval4lem1  46647  lamberte  46889  i0oii  48908  io1ii  48909  2arwcatlem4  49587  2arwcat  49589