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

Theorem csbeq1 2976
Description: Analog of dfsbcq 2882 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )

Proof of Theorem csbeq1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 2882 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2233 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 2974 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 2974 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2173 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    e. wcel 1463   {cab 2101   [.wsbc 2880   [_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:  csbeq1d  2979  csbeq1a  2981  csbiebg  3010  sbcnestgf  3019  cbvralcsf  3030  cbvrexcsf  3031  cbvreucsf  3032  cbvrabcsf  3033  csbing  3251  disjnims  3889  sbcbrg  3950  csbopabg  3974  pofun  4202  csbima12g  4868  csbiotag  5084  fvmpts  5465  fvmpt2  5470  mptfvex  5472  elfvmptrab1  5481  fmptcof  5553  fmptcos  5554  fliftfuns  5665  csbriotag  5708  csbov123g  5775  eqerlem  6426  qliftfuns  6479  summodclem2a  11090  zsumdc  11093  fsum3  11096  sumsnf  11118  sumsns  11124  fsum2dlemstep  11143  fisumcom2  11147  fsumshftm  11154  fisum0diag2  11156  fsumiun  11186  ctiunctlemf  11846  mulcncflem  12654
  Copyright terms: Public domain W3C validator