![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbcieg | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit class substitution. (Contributed by NM, 10-Nov-2005.) |
Ref | Expression |
---|---|
sbcieg.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sbcieg |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1771 |
. 2
![]() ![]() ![]() ![]() | |
2 | sbcieg.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | sbciegf 3310 |
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-12 1943 ax-13 2101 ax-ext 2441 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1457 df-ex 1674 df-nf 1678 df-sb 1808 df-clab 2448 df-cleq 2454 df-clel 2457 df-v 3058 df-sbc 3279 |
This theorem is referenced by: sbcie 3313 ralsng 4017 rexsng 4018 rabsnif 4053 ralrnmpt 6053 fpwwe2lem3 9083 nn1suc 10657 mrcmndind 16661 fgcl 20941 cfinfil 20956 csdfil 20957 supfil 20958 fin1aufil 20995 ifeqeqx 28206 nn0min 28432 bnj1452 29909 cdlemk35s 34548 cdlemk39s 34550 cdlemk42 34552 2nn0ind 35837 zindbi 35838 trsbcVD 37313 onfrALTlem5VD 37321 |
Copyright terms: Public domain | W3C validator |