![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcbii | Structured version Visualization 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 3333 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | trud 1463 |
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 1679 ax-4 1692 ax-5 1768 ax-6 1815 ax-7 1861 ax-10 1925 ax-11 1930 ax-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-sbc 3279 |
This theorem is referenced by: eqsbc3r 3335 sbc3an 3336 sbccomlem 3349 sbccom 3350 sbcrext 3352 sbcabel 3356 csbco 3384 sbcnel12g 3785 sbcne12 3786 csbcom 3794 csbnestgf 3796 sbccsb 3804 sbccsb2 3805 csbab 3808 sbcssg 3891 sbcrel 4939 difopab 4984 sbcfung 5623 tfinds2 6716 mpt2xopovel 6992 f1od2 28357 bnj62 29574 bnj89 29575 bnj156 29584 bnj524 29594 bnj538OLD 29598 bnj610 29605 bnj919 29626 bnj976 29637 bnj110 29717 bnj91 29720 bnj92 29721 bnj106 29727 bnj121 29729 bnj124 29730 bnj125 29731 bnj126 29732 bnj130 29733 bnj154 29737 bnj155 29738 bnj153 29739 bnj207 29740 bnj523 29746 bnj526 29747 bnj539 29750 bnj540 29751 bnj581 29767 bnj591 29770 bnj609 29776 bnj611 29777 bnj934 29794 bnj1000 29800 bnj984 29811 bnj985 29812 bnj1040 29829 bnj1123 29843 bnj1452 29909 bnj1463 29912 sbcalf 32396 sbcexf 32397 sbccom2lem 32408 sbccom2 32409 sbccom2f 32410 sbccom2fi 32411 csbcom2fi 32413 2sbcrex 35671 2sbcrexOLD 35673 sbcrot3 35678 sbcrot5 35679 2rexfrabdioph 35683 3rexfrabdioph 35684 4rexfrabdioph 35685 6rexfrabdioph 35686 7rexfrabdioph 35687 rmydioph 35913 expdiophlem2 35921 sbcheg 36418 sbc3or 36932 sbcbiiOLD 36935 trsbc 36944 onfrALTlem5 36951 csbabgOLD 37250 |
Copyright terms: Public domain | W3C validator |