Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > csbeq1a | Unicode version |
Description: Equality theorem for proper substitution into a class. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
csbeq1a |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | csbid 2982 | . 2 | |
2 | csbeq1 2978 | . 2 | |
3 | 1, 2 | syl5eqr 2164 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wceq 1316 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: csbhypf 3008 csbiebt 3009 sbcnestgf 3021 cbvralcsf 3032 cbvrexcsf 3033 cbvreucsf 3034 cbvrabcsf 3035 csbing 3253 disjnims 3891 disjiun 3894 sbcbrg 3952 moop2 4143 pofun 4204 eusvnf 4344 opeliunxp 4564 elrnmpt1 4760 resmptf 4839 csbima12g 4870 fvmpts 5467 fvmpt2 5472 mptfvex 5474 fmptco 5554 fmptcof 5555 fmptcos 5556 elabrex 5627 fliftfuns 5667 csbov123g 5777 ovmpos 5862 csbopeq1a 6054 mpomptsx 6063 dmmpossx 6065 fmpox 6066 mpofvex 6069 fmpoco 6081 disjxp1 6101 eqerlem 6428 qliftfuns 6481 mptelixpg 6596 xpf1o 6706 iunfidisj 6802 seq3f1olemstep 10242 seq3f1olemp 10243 sumeq2 11096 sumfct 11111 sumrbdclem 11113 summodclem3 11117 summodclem2a 11118 zsumdc 11121 fsumgcl 11123 fsum3 11124 isumss 11128 isumss2 11130 fsum3cvg2 11131 fsumzcl2 11142 fsumsplitf 11145 sumsnf 11146 sumsns 11152 fsumsplitsnun 11156 fsum2dlemstep 11171 fsumcnv 11174 fisumcom2 11175 fsumshftm 11182 fisum0diag2 11184 fsummulc2 11185 fsum00 11199 fsumabs 11202 fsumrelem 11208 fsumiun 11214 isumshft 11227 mertenslem2 11273 ctiunctlemudc 11877 ctiunctlemf 11878 iuncld 12211 fsumcncntop 12652 limcmpted 12728 |
Copyright terms: Public domain | W3C validator |