![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfcii | Structured version Visualization version GIF 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 2115 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
3 | 2 | nfci 2934 | 1 ⊢ Ⅎ𝑥𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1518 ∈ wcel 2079 Ⅎwnfc 2931 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1775 ax-4 1789 ax-10 2110 |
This theorem depends on definitions: df-bi 208 df-ex 1760 df-nf 1764 df-nfc 2933 |
This theorem is referenced by: bnj1316 31665 bnj1385 31677 bnj1400 31680 bnj1468 31690 bnj1534 31697 bnj1542 31701 bnj1228 31853 bnj1307 31865 bnj1448 31889 bnj1466 31895 bnj1463 31897 bnj1491 31899 bnj1312 31900 bnj1498 31903 bnj1520 31908 bnj1525 31911 bnj1529 31912 bnj1523 31913 |
Copyright terms: Public domain | W3C validator |