Theorem eqeltrrid 2317

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 2233	. 2 ⊢ 𝐴 = 𝐵
3		eqeltrrid.2	. 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶)
4	2, 3	eqeltrid 2316	1 ⊢ (𝜑 → 𝐴 ∈ 𝐶)

Syntax hints:   → wi 4   = wceq 1395   ∈ wcel 2200

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 1493  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-cleq 2222  df-clel 2225

This theorem is referenced by:  dmrnssfld  4993  cnvexg  5272  opabbrex  6060  offval  6238  resfunexgALT  6265  abrexexg  6275  abrexex2g  6277  opabex3d  6278  oprssdmm  6329  unfidisj  7107  residfi  7130  ssfii  7164  djuexb  7234  nqprlu  7757  iccshftr  10219  iccshftl  10221  iccdil  10223  icccntr  10225  mertenslem2  12087  exprmfct  12700  infpnlem1  12922  4sqlem13m  12966  ennnfonelemg  13014  prdsval  13346  prdsbaslemss  13347  grpidvalg  13446  igsumvalx  13462  grppropstrg  13592  releqgg  13797  eqgex  13798  0opn  14720  difopn  14822  tgrest  14883  txbasex  14971  txdis1cn  14992  cnmptid  14995  cnmptc  14996  cnmpt1st  15002  cnmpt2nd  15003  cnmpt2c  15004  hmeoima  15024  hmeocld  15026  fsumcncntop  15281  expcn  15283  plycoeid3  15471