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

Theorem csbeq1a 2981
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 2980 . 2  |-  [_ x  /  x ]_ B  =  B
2 csbeq1 2976 . 2  |-  ( x  =  A  ->  [_ x  /  x ]_ B  = 
[_ A  /  x ]_ B )
31, 2syl5eqr 2162 1  |-  ( x  =  A  ->  B  =  [_ A  /  x ]_ B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314   [_csb 2973
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-tru 1317  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-sbc 2881  df-csb 2974
This theorem is referenced by:  csbhypf  3006  csbiebt  3007  sbcnestgf  3019  cbvralcsf  3030  cbvrexcsf  3031  cbvreucsf  3032  cbvrabcsf  3033  csbing  3251  disjnims  3889  disjiun  3892  sbcbrg  3950  moop2  4141  pofun  4202  eusvnf  4342  opeliunxp  4562  elrnmpt1  4758  resmptf  4837  csbima12g  4868  fvmpts  5465  fvmpt2  5470  mptfvex  5472  fmptco  5552  fmptcof  5553  fmptcos  5554  elabrex  5625  fliftfuns  5665  csbov123g  5775  ovmpos  5860  csbopeq1a  6052  mpomptsx  6061  dmmpossx  6063  fmpox  6064  mpofvex  6067  fmpoco  6079  disjxp1  6099  eqerlem  6426  qliftfuns  6479  mptelixpg  6594  xpf1o  6704  iunfidisj  6800  seq3f1olemstep  10214  seq3f1olemp  10215  sumeq2  11068  sumfct  11083  sumrbdclem  11085  summodclem3  11089  summodclem2a  11090  zsumdc  11093  fsumgcl  11095  fsum3  11096  isumss  11100  isumss2  11102  fsum3cvg2  11103  fsumzcl2  11114  fsumsplitf  11117  sumsnf  11118  sumsns  11124  fsumsplitsnun  11128  fsum2dlemstep  11143  fsumcnv  11146  fisumcom2  11147  fsumshftm  11154  fisum0diag2  11156  fsummulc2  11157  fsum00  11171  fsumabs  11174  fsumrelem  11180  fsumiun  11186  isumshft  11199  mertenslem2  11245  ctiunctlemudc  11845  ctiunctlemf  11846  iuncld  12179  fsumcncntop  12620  limcmpted  12684
  Copyright terms: Public domain W3C validator