Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > nfcii | Structured version Visualization version Unicode version |
Description: Deduce that a class does not have free in it. (Contributed by Mario Carneiro, 11-Aug-2016.) |
Ref | Expression |
---|---|
nfcii.1 |
Ref | Expression |
---|---|
nfcii |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfcii.1 | . . 3 | |
2 | 1 | nf5i 2024 | . 2 |
3 | 2 | nfci 2754 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wal 1481 wcel 1990 wnfc 2751 |
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-10 2019 |
This theorem depends on definitions: df-bi 197 df-ex 1705 df-nf 1710 df-nfc 2753 |
This theorem is referenced by: bnj1316 30891 bnj1385 30903 bnj1400 30906 bnj1468 30916 bnj1534 30923 bnj1542 30927 bnj1228 31079 bnj1307 31091 bnj1448 31115 bnj1466 31121 bnj1463 31123 bnj1491 31125 bnj1312 31126 bnj1498 31129 bnj1520 31134 bnj1525 31137 bnj1529 31138 bnj1523 31139 |
Copyright terms: Public domain | W3C validator |