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  4987  cnvexg  5266  opabbrex  6054  offval  6232  resfunexgALT  6259  abrexexg  6269  abrexex2g  6271  opabex3d  6272  oprssdmm  6323  unfidisj  7095  residfi  7118  ssfii  7152  djuexb  7222  nqprlu  7745  iccshftr  10202  iccshftl  10204  iccdil  10206  icccntr  10208  mertenslem2  12063  exprmfct  12676  infpnlem1  12898  4sqlem13m  12942  ennnfonelemg  12990  prdsval  13322  prdsbaslemss  13323  grpidvalg  13422  igsumvalx  13438  grppropstrg  13568  releqgg  13773  eqgex  13774  0opn  14696  difopn  14798  tgrest  14859  txbasex  14947  txdis1cn  14968  cnmptid  14971  cnmptc  14972  cnmpt1st  14978  cnmpt2nd  14979  cnmpt2c  14980  hmeoima  15000  hmeocld  15002  fsumcncntop  15257  expcn  15259  plycoeid3  15447