Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcied | Structured version Visualization version Unicode version |
Description: Conversion of implicit substitution to explicit class substitution, deduction form. (Contributed by NM, 13-Dec-2014.) |
Ref | Expression |
---|---|
sbcied.1 | |
sbcied.2 |
Ref | Expression |
---|---|
sbcied |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcied.1 | . 2 | |
2 | sbcied.2 | . 2 | |
3 | nfv 1843 | . 2 | |
4 | nfvd 1844 | . 2 | |
5 | 1, 2, 3, 4 | sbciedf 3471 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 wa 384 wceq 1483 wcel 1990 wsbc 3435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-v 3202 df-sbc 3436 |
This theorem is referenced by: sbcied2 3473 sbc2iedv 3506 sbc3ie 3507 sbcralt 3510 euotd 4975 fmptsnd 6435 riota5f 6636 fpwwe2lem12 9463 fpwwe2lem13 9464 brfi1uzind 13280 opfi1uzind 13283 brfi1uzindOLD 13286 opfi1uzindOLD 13289 sbcie3s 15917 issubc 16495 gsumvalx 17270 dmdprd 18397 dprdval 18402 issrg 18507 issrng 18850 islmhm 19027 isassa 19315 isphl 19973 istmd 21878 istgp 21881 isnlm 22479 isclm 22864 iscph 22970 iscms 23142 limcfval 23636 ewlksfval 26497 sbcies 29322 abfmpeld 29454 abfmpel 29455 isomnd 29701 isorng 29799 |
Copyright terms: Public domain | W3C validator |