![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > nfcsb | Structured version Unicode version |
Description: Bound-variable hypothesis builder for substitution into a class. (Contributed by Mario Carneiro, 12-Oct-2016.) |
Ref | Expression |
---|---|
nfcsb.1 |
![]() ![]() ![]() ![]() |
nfcsb.2 |
![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
nfcsb |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nftru 1600 |
. . 3
![]() ![]() ![]() ![]() | |
2 | nfcsb.1 |
. . . 4
![]() ![]() ![]() ![]() | |
3 | 2 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | nfcsb.2 |
. . . 4
![]() ![]() ![]() ![]() | |
5 | 4 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 1, 3, 5 | nfcsbd 3413 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
7 | 6 | 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 1955 ax-ext 2432 |
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 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-sbc 3295 df-csb 3397 |
This theorem is referenced by: cbvralcsf 3428 cbvreucsf 3430 cbvrabcsf 3431 fmptcof 5987 mpt2mptsx 6748 dmmpt2ssx 6750 fmpt2x 6751 fmpt2co 6767 dfmpt2 6774 mpt2curryd 6899 fvmpt2curryd 6901 nfsum 13287 fsum2dlem 13356 fsumcom2 13360 fsumcn 20579 fsum2cn 20580 dvmptfsum 21581 itgsubst 21655 iundisj2f 26084 f1od2 26176 nfcprod 27569 fprod2dlem 27636 fprodcom2 27640 wdom2d2 29533 elfvmptrab1 30303 elovmpt2rab1 30308 dmmpt2ssx2 30876 cdlemkid 34919 cdlemk19x 34926 cdlemk11t 34929 |
Copyright terms: Public domain | W3C validator |