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

Theorem csbeq1 2828
Description: Analog of dfsbcq 2739 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.)
Assertion
Ref Expression
csbeq1  [_  ]_ C 
[_  ]_ C

Proof of Theorem csbeq1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 dfsbcq 2739 . . 3  [.  ].  C  [.  ].  C
21abbidv 2133 . 2  {  |  [.  ].  C }  {  |  [.  ].  C }
3 df-csb 2826 . 2  [_  ]_ C  {  |  [.  ].  C }
4 df-csb 2826 . 2  [_  ]_ C  {  |  [.  ].  C }
52, 3, 43eqtr4g 2075 1  [_  ]_ C 
[_  ]_ C
Colors of variables: wff set class
Syntax hints:   wi 4   wceq 1226   wcel 1370   {cab 2004   [.wsbc 2737   [_csb 2825
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1312  ax-7 1313  ax-gen 1314  ax-ie1 1359  ax-ie2 1360  ax-8 1372  ax-11 1374  ax-4 1377  ax-17 1396  ax-i9 1400  ax-ial 1405  ax-i5r 1406  ax-ext 2000
This theorem depends on definitions:  df-bi 110  df-tru 1229  df-nf 1326  df-sb 1624  df-clab 2005  df-cleq 2011  df-clel 2014  df-sbc 2738  df-csb 2826
This theorem is referenced by:  csbeq1d  2831  csbeq1a  2833  csbiebg  2862  sbcnestgf  2870  cbvralcsf  2881  cbvrexcsf  2882  cbvreucsf  2883  cbvrabcsf  2884  csbing  3117  sbcbrg  3783  csbopabg  3805  pofun  4019  csbima12g  4609  csbiotag  4818  fvmpts  5171  fvmpt2  5175  mptfvex  5177  fmptcof  5252  fmptcos  5253  fliftfuns  5359  csbriotag  5400  csbov123g  5462  eqerlem  6044  qliftfuns  6097
  Copyright terms: Public domain W3C validator