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

Theorem eqeltrid 2226
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrid.1  |-  A  =  B
eqeltrid.2  |-  ( ph  ->  B  e.  C )
Assertion
Ref Expression
eqeltrid  |-  ( ph  ->  A  e.  C )

Proof of Theorem eqeltrid
StepHypRef Expression
1 eqeltrid.1 . . 3  |-  A  =  B
21a1i 9 . 2  |-  ( ph  ->  A  =  B )
3 eqeltrid.2 . 2  |-  ( ph  ->  B  e.  C )
42, 3eqeltrd 2216 1  |-  ( ph  ->  A  e.  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1331    e. wcel 1480
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-cleq 2132  df-clel 2135
This theorem is referenced by:  eqeltrrid  2227  csbexga  4056  otexg  4152  tpexg  4365  dmresexg  4842  f1oabexg  5379  funfvex  5438  riotaexg  5734  riotaprop  5753  fnovex  5804  ovexg  5805  fovrn  5913  fnovrn  5918  cofunexg  6009  cofunex2g  6010  abrexex2g  6018  xpexgALT  6031  mpofvex  6101  tfrex  6265  frec0g  6294  freccllem  6299  ecexg  6433  qsexg  6485  pmex  6547  elixpsn  6629  diffifi  6788  unfidisj  6810  prfidisj  6815  tpfidisj  6816  ssfirab  6822  ssfidc  6823  fnfi  6825  funrnfi  6830  iunfidisj  6834  infclti  6910  djuex  6928  ctssdccl  6996  addvalex  7659  negcl  7969  intqfrac2  10099  intfracq  10100  frec2uzzd  10180  frecuzrdgrrn  10188  iseqf1olemqpcl  10276  seq3f1olemqsum  10280  bcval5  10516  xrmaxiflemval  11026  climmpt  11076  reccn2ap  11089  zsumdc  11160  fsumzcl2  11181  fsump1i  11209  fsumabs  11241  hash2iun1dif1  11256  mertenslemi1  11311  algrf  11733  algcvg  11736  algcvga  11739  algfx  11740  eucalgcvga  11746  eucalg  11747  crth  11907  phimullem  11908  ennnfonelemj0  11921  ennnfonelemom  11928  ressid  12030  1strbas  12068  2strbasg  12070  2stropg  12071  restid  12141  topnvalg  12142  topnidg  12143  topopn  12185  topcld  12288  uncld  12292  iuncld  12294  unicld  12295  tgrest  12348  restin  12355  cnco  12400  cnrest  12414  cnptoprest2  12419  lmss  12425  txbasval  12446  txcn  12454  cnmpt12f  12465  hmeoco  12495  idhmeo  12496  blres  12613  metrest  12685  qtopbasss  12700  tgqioo  12726  divcnap  12734  fsumcncntop  12735  cncfmet  12758  cdivcncfap  12766  cnrehmeocntop  12772  cnplimcim  12815  limccnpcntop  12823  limccnp2lem  12824  limccnp2cntop  12825  dvfvalap  12829  bj-snexg  13140  trilpolemcl  13260
  Copyright terms: Public domain W3C validator