Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > sbcan | Structured version Visualization version Unicode version |
Description: Distribution of class substitution over conjunction. (Contributed by NM, 31-Dec-2016.) (Revised by NM, 17-Aug-2018.) |
Ref | Expression |
---|---|
sbcan |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbcex 3445 | . 2 | |
2 | sbcex 3445 | . . 3 | |
3 | 2 | adantl 482 | . 2 |
4 | dfsbcq2 3438 | . . 3 | |
5 | dfsbcq2 3438 | . . . 4 | |
6 | dfsbcq2 3438 | . . . 4 | |
7 | 5, 6 | anbi12d 747 | . . 3 |
8 | sban 2399 | . . 3 | |
9 | 4, 7, 8 | vtoclbg 3267 | . 2 |
10 | 1, 3, 9 | pm5.21nii 368 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wb 196 wa 384 wceq 1483 wsb 1880 wcel 1990 cvv 3200 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-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: sbc3an 3494 sbcabel 3517 csbopg 4420 csbuni 4466 csbmpt12 5010 csbxp 5200 difopab 5253 sbcfung 5912 sbcfng 6042 sbcfg 6043 fmptsnd 6435 f1od2 29499 esum2dlem 30154 bnj976 30848 bnj110 30928 bnj1040 31040 csbwrecsg 33173 csboprabg 33176 csbmpt22g 33177 f1omptsnlem 33183 mptsnunlem 33185 relowlpssretop 33212 csbfinxpg 33225 sbcani 33910 sbccom2lem 33929 brtrclfv2 38019 cotrclrcl 38034 frege124d 38053 sbiota1 38635 onfrALTlem5 38757 onfrALTlem4 38758 |
Copyright terms: Public domain | W3C validator |