![]() |
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 2142 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
3 | 2 | nfci 2886 | 1 ⊢ Ⅎ𝑥𝐴 |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∀wal 1539 ∈ wcel 2106 Ⅎwnfc 2883 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-10 2137 |
This theorem depends on definitions: df-bi 206 df-ex 1782 df-nf 1786 df-nfc 2885 |
This theorem is referenced by: bnj1316 33726 bnj1385 33738 bnj1400 33741 bnj1468 33752 bnj1534 33759 bnj1542 33763 bnj1228 33917 bnj1307 33929 bnj1448 33953 bnj1466 33959 bnj1463 33961 bnj1491 33963 bnj1312 33964 bnj1498 33967 bnj1520 33972 bnj1525 33975 bnj1529 33976 bnj1523 33977 |
Copyright terms: Public domain | W3C validator |