ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqeltrrid GIF version

Theorem eqeltrrid 2293
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
StepHypRef Expression
1 eqeltrrid.1 . . 3 𝐵 = 𝐴
21eqcomi 2209 . 2 𝐴 = 𝐵
3 eqeltrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrid 2292 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1373  wcel 2176
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 1470  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-4 1533  ax-17 1549  ax-ial 1557  ax-ext 2187
This theorem depends on definitions:  df-bi 117  df-cleq 2198  df-clel 2201
This theorem is referenced by:  dmrnssfld  4941  cnvexg  5220  opabbrex  5989  offval  6166  resfunexgALT  6193  abrexexg  6203  abrexex2g  6205  opabex3d  6206  oprssdmm  6257  unfidisj  7019  residfi  7042  ssfii  7076  djuexb  7146  nqprlu  7660  iccshftr  10116  iccshftl  10118  iccdil  10120  icccntr  10122  mertenslem2  11847  exprmfct  12460  infpnlem1  12682  4sqlem13m  12726  ennnfonelemg  12774  prdsval  13105  prdsbaslemss  13106  grpidvalg  13205  igsumvalx  13221  grppropstrg  13351  releqgg  13556  eqgex  13557  0opn  14478  difopn  14580  tgrest  14641  txbasex  14729  txdis1cn  14750  cnmptid  14753  cnmptc  14754  cnmpt1st  14760  cnmpt2nd  14761  cnmpt2c  14762  hmeoima  14782  hmeocld  14784  fsumcncntop  15039  expcn  15041  plycoeid3  15229
  Copyright terms: Public domain W3C validator