![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > csbeq1 | Unicode version |
Description: Analog of dfsbcq 2915 for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfsbcq 2915 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | abbidv 2258 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | df-csb 3008 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | df-csb 3008 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 2, 3, 4 | 3eqtr4g 2198 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() ![]() ![]() |
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 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-clel 2136 df-sbc 2914 df-csb 3008 |
This theorem is referenced by: csbeq1d 3014 csbeq1a 3016 csbiebg 3047 sbcnestgf 3056 cbvralcsf 3067 cbvrexcsf 3068 cbvreucsf 3069 cbvrabcsf 3070 csbing 3288 disjnims 3929 sbcbrg 3990 csbopabg 4014 pofun 4242 csbima12g 4908 csbiotag 5124 fvmpts 5507 fvmpt2 5512 mptfvex 5514 elfvmptrab1 5523 fmptcof 5595 fmptcos 5596 fliftfuns 5707 csbriotag 5750 csbov123g 5817 eqerlem 6468 qliftfuns 6521 summodclem2a 11182 zsumdc 11185 fsum3 11188 sumsnf 11210 sumsns 11216 fsum2dlemstep 11235 fisumcom2 11239 fsumshftm 11246 fisum0diag2 11248 fsumiun 11278 ctiunctlemf 11987 mulcncflem 12798 |
Copyright terms: Public domain | W3C validator |