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

Theorem csbeq1 2978
Description: Analog of dfsbcq 2884 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 2884 . . 3  |-  ( A  =  B  ->  ( [. A  /  x ]. y  e.  C  <->  [. B  /  x ]. y  e.  C )
)
21abbidv 2235 . 2  |-  ( A  =  B  ->  { y  |  [. A  /  x ]. y  e.  C }  =  { y  |  [. B  /  x ]. y  e.  C } )
3 df-csb 2976 . 2  |-  [_ A  /  x ]_ C  =  { y  |  [. A  /  x ]. y  e.  C }
4 df-csb 2976 . 2  |-  [_ B  /  x ]_ C  =  { y  |  [. B  /  x ]. y  e.  C }
52, 3, 43eqtr4g 2175 1  |-  ( A  =  B  ->  [_ A  /  x ]_ C  = 
[_ B  /  x ]_ C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    e. wcel 1465   {cab 2103   [.wsbc 2882   [_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:  csbeq1d  2981  csbeq1a  2983  csbiebg  3012  sbcnestgf  3021  cbvralcsf  3032  cbvrexcsf  3033  cbvreucsf  3034  cbvrabcsf  3035  csbing  3253  disjnims  3891  sbcbrg  3952  csbopabg  3976  pofun  4204  csbima12g  4870  csbiotag  5086  fvmpts  5467  fvmpt2  5472  mptfvex  5474  elfvmptrab1  5483  fmptcof  5555  fmptcos  5556  fliftfuns  5667  csbriotag  5710  csbov123g  5777  eqerlem  6428  qliftfuns  6481  summodclem2a  11118  zsumdc  11121  fsum3  11124  sumsnf  11146  sumsns  11152  fsum2dlemstep  11171  fisumcom2  11175  fsumshftm  11182  fisum0diag2  11184  fsumiun  11214  ctiunctlemf  11878  mulcncflem  12686
  Copyright terms: Public domain W3C validator