![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > sbcbii | Structured version Unicode version |
Description: Formula-building inference rule for class substitution. (Contributed by NM, 11-Nov-2005.) |
Ref | Expression |
---|---|
sbcbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sbcbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | sbcbidv 3343 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | trud 1379 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1952 ax-ext 2430 |
This theorem depends on definitions: df-bi 185 df-an 371 df-tru 1373 df-ex 1588 df-nf 1591 df-sb 1703 df-clab 2437 df-cleq 2443 df-clel 2446 df-sbc 3285 |
This theorem is referenced by: sbcbiiOLD 3345 eqsbc3r 3346 sbc3an 3347 sbccomlem 3363 sbccom 3364 sbcrextOLD 3366 sbcrext 3367 sbcabel 3373 csbco 3396 sbcnel12g 3776 sbcne12 3777 sbcne12gOLD 3778 csbcom 3787 csbnestgf 3790 sbccsb 3799 sbccsbgOLD 3800 sbccsb2 3801 sbccsb2gOLD 3802 csbab 3805 csbabgOLD 3806 sbcssg 3888 sbcrel 5024 difopab 5069 sbcfung 5539 tfinds2 6574 mpt2xopovel 6837 f1od2 26158 sbcalf 29058 sbcexf 29059 sbccom2lem 29071 sbccom2 29072 sbccom2f 29073 sbccom2fi 29074 csbcom2fi 29076 2sbcrex 29261 2sbcrexOLD 29262 sbcrot3 29267 sbcrot5 29268 2rexfrabdioph 29272 3rexfrabdioph 29273 4rexfrabdioph 29274 6rexfrabdioph 29275 7rexfrabdioph 29276 rmydioph 29501 expdiophlem2 29509 sbc3or 31537 trsbc 31547 onfrALTlem5 31550 bnj62 32009 bnj89 32010 bnj156 32019 bnj524 32029 bnj538 32032 bnj610 32039 bnj919 32060 bnj976 32071 bnj110 32151 bnj91 32154 bnj92 32155 bnj106 32161 bnj121 32163 bnj124 32164 bnj125 32165 bnj126 32166 bnj130 32167 bnj154 32171 bnj155 32172 bnj153 32173 bnj207 32174 bnj523 32180 bnj526 32181 bnj539 32184 bnj540 32185 bnj581 32201 bnj591 32204 bnj609 32210 bnj611 32211 bnj934 32228 bnj1000 32234 bnj984 32245 bnj985 32246 bnj1040 32263 bnj1123 32277 bnj1452 32343 bnj1463 32346 |
Copyright terms: Public domain | W3C validator |