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

Theorem csbeq1a 2983
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1a  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )

Proof of Theorem csbeq1a
StepHypRef Expression
1 csbid 2982 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 2978 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2164 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316   [_csb 2975
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 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-sbc 2883  df-csb 2976
This theorem is referenced by:  csbhypf  3008  csbiebt  3009  sbcnestgf  3021  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  csbing  3253  disjnims  3891  disjiun  3894  sbcbrg  3952  moop2  4143  pofun  4204  eusvnf  4344  opeliunxp  4564  elrnmpt1  4760  resmptf  4839  csbima12g  4870  fvmpts  5467  fvmpt2  5472  mptfvex  5474  fmptco  5554  fmptcof  5555  fmptcos  5556  elabrex  5627  fliftfuns  5667  csbov123g  5777  ovmpos  5862  csbopeq1a  6054  mpomptsx  6063  dmmpossx  6065  fmpox  6066  mpofvex  6069  fmpoco  6081  disjxp1  6101  eqerlem  6428  qliftfuns  6481  mptelixpg  6596  xpf1o  6706  iunfidisj  6802  seq3f1olemstep  10242  seq3f1olemp  10243  sumeq2  11096  sumfct  11111  sumrbdclem  11113  summodclem3  11117  summodclem2a  11118  zsumdc  11121  fsumgcl  11123  fsum3  11124  isumss  11128  isumss2  11130  fsum3cvg2  11131  fsumzcl2  11142  fsumsplitf  11145  sumsnf  11146  sumsns  11152  fsumsplitsnun  11156  fsum2dlemstep  11171  fsumcnv  11174  fisumcom2  11175  fsumshftm  11182  fisum0diag2  11184  fsummulc2  11185  fsum00  11199  fsumabs  11202  fsumrelem  11208  fsumiun  11214  isumshft  11227  mertenslem2  11273  ctiunctlemudc  11877  ctiunctlemf  11878  iuncld  12211  fsumcncntop  12652  limcmpted  12728
  Copyright terms: Public domain W3C validator