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

Theorem eqeltrid 2224
Description: B membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
eqeltrid.1 𝐴 = 𝐵
eqeltrid.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
eqeltrid (𝜑𝐴𝐶)

Proof of Theorem eqeltrid
StepHypRef Expression
1 eqeltrid.1 . . 3 𝐴 = 𝐵
21a1i 9 . 2 (𝜑𝐴 = 𝐵)
3 eqeltrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqeltrd 2214 1 (𝜑𝐴𝐶)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  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 2119
This theorem depends on definitions:  df-bi 116  df-cleq 2130  df-clel 2133
This theorem is referenced by:  eqeltrrid  2225  csbexga  4051  otexg  4147  tpexg  4360  dmresexg  4837  f1oabexg  5372  funfvex  5431  riotaexg  5727  riotaprop  5746  fnovex  5797  ovexg  5798  fovrn  5906  fnovrn  5911  cofunexg  6002  cofunex2g  6003  abrexex2g  6011  xpexgALT  6024  mpofvex  6094  tfrex  6258  frec0g  6287  freccllem  6292  ecexg  6426  qsexg  6478  pmex  6540  elixpsn  6622  diffifi  6781  unfidisj  6803  prfidisj  6808  tpfidisj  6809  ssfirab  6815  ssfidc  6816  fnfi  6818  funrnfi  6823  iunfidisj  6827  infclti  6903  djuex  6921  ctssdccl  6989  addvalex  7645  negcl  7955  intqfrac2  10085  intfracq  10086  frec2uzzd  10166  frecuzrdgrrn  10174  iseqf1olemqpcl  10262  seq3f1olemqsum  10266  bcval5  10502  xrmaxiflemval  11012  climmpt  11062  reccn2ap  11075  zsumdc  11146  fsumzcl2  11167  fsump1i  11195  fsumabs  11227  hash2iun1dif1  11242  mertenslemi1  11297  algrf  11715  algcvg  11718  algcvga  11721  algfx  11722  eucalgcvga  11728  eucalg  11729  crth  11889  phimullem  11890  ennnfonelemj0  11903  ennnfonelemom  11910  ressid  12009  1strbas  12047  2strbasg  12049  2stropg  12050  restid  12120  topnvalg  12121  topnidg  12122  topopn  12164  topcld  12267  uncld  12271  iuncld  12273  unicld  12274  tgrest  12327  restin  12334  cnco  12379  cnrest  12393  cnptoprest2  12398  lmss  12404  txbasval  12425  txcn  12433  cnmpt12f  12444  hmeoco  12474  idhmeo  12475  blres  12592  metrest  12664  qtopbasss  12679  tgqioo  12705  divcnap  12713  fsumcncntop  12714  cncfmet  12737  cdivcncfap  12745  cnrehmeocntop  12751  cnplimcim  12794  limccnpcntop  12802  limccnp2lem  12803  limccnp2cntop  12804  dvfvalap  12808  bj-snexg  13099  trilpolemcl  13219
  Copyright terms: Public domain W3C validator