Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > csbeq1 | Unicode version |
Description: Analog of dfsbcq 2939 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2939 | . . 3 | |
2 | 1 | abbidv 2275 | . 2 |
3 | df-csb 3032 | . 2 | |
4 | df-csb 3032 | . 2 | |
5 | 2, 3, 4 | 3eqtr4g 2215 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1335 wcel 2128 cab 2143 wsbc 2937 csb 3031 |
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 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-11 1486 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-tru 1338 df-nf 1441 df-sb 1743 df-clab 2144 df-cleq 2150 df-clel 2153 df-sbc 2938 df-csb 3032 |
This theorem is referenced by: csbeq1d 3038 csbeq1a 3040 csbiebg 3073 sbcnestgf 3082 cbvralcsf 3093 cbvrexcsf 3094 cbvreucsf 3095 cbvrabcsf 3096 csbing 3314 disjnims 3957 sbcbrg 4018 csbopabg 4042 pofun 4272 csbima12g 4946 csbiotag 5162 fvmpts 5545 fvmpt2 5550 mptfvex 5552 elfvmptrab1 5561 fmptcof 5633 fmptcos 5634 fliftfuns 5745 csbriotag 5789 csbov123g 5856 eqerlem 6508 qliftfuns 6561 summodclem2a 11273 zsumdc 11276 fsum3 11279 sumsnf 11301 sumsns 11307 fsum2dlemstep 11326 fisumcom2 11330 fsumshftm 11337 fisum0diag2 11339 fsumiun 11369 prodsnf 11484 fprodm1s 11493 fprodp1s 11494 prodsns 11495 fprod2dlemstep 11514 fprodcom2fi 11518 ctiunctlemf 12154 mulcncflem 12977 |
Copyright terms: Public domain | W3C validator |