Theorem eqeltrrid 2284

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

Hypotheses

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

Assertion

Ref	Expression
eqeltrrid	⊢ (𝜑 → 𝐴 ∈ 𝐶)

Proof of Theorem eqeltrrid

Step	Hyp	Ref	Expression
1		eqeltrrid.1	. . 3 ⊢ 𝐵 = 𝐴
2	1	eqcomi 2200	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2283	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1364   ∈ wcel 2167

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1461  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-cleq 2189  df-clel 2192

This theorem is referenced by:  dmrnssfld  4930  cnvexg  5208  opabbrex  5970  offval  6147  resfunexgALT  6174  abrexexg  6184  abrexex2g  6186  opabex3d  6187  oprssdmm  6238  unfidisj  6992  residfi  7015  ssfii  7049  djuexb  7119  nqprlu  7631  iccshftr  10086  iccshftl  10088  iccdil  10090  icccntr  10092  mertenslem2  11718  exprmfct  12331  infpnlem1  12553  4sqlem13m  12597  ennnfonelemg  12645  prdsval  12975  prdsbaslemss  12976  grpidvalg  13075  igsumvalx  13091  grppropstrg  13221  releqgg  13426  eqgex  13427  0opn  14326  difopn  14428  tgrest  14489  txbasex  14577  txdis1cn  14598  cnmptid  14601  cnmptc  14602  cnmpt1st  14608  cnmpt2nd  14609  cnmpt2c  14610  hmeoima  14630  hmeocld  14632  fsumcncntop  14887  expcn  14889  plycoeid3  15077