![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > nfci | 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 |
---|---|
nfci.1 | ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 |
Ref | Expression |
---|---|
nfci | ⊢ Ⅎ𝑥𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-nfc 2885 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
2 | nfci.1 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | |
3 | 1, 2 | mpgbir 1801 | 1 ⊢ Ⅎ𝑥𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1785 ∈ 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 |
This theorem depends on definitions: df-bi 206 df-nfc 2885 |
This theorem is referenced by: nfcii 2887 nfcv 2903 nfab1 2905 nfab 2909 nfabg 2910 iinabrex 31729 fpwrelmap 31893 esumfzf 32962 fsumiunss 44128 climsuse 44161 climinff 44164 fnlimfvre 44227 limsupre3uzlem 44288 pimdecfgtioc 45268 pimincfltioc 45269 smfmullem4 45347 smflimsupmpt 45382 |
Copyright terms: Public domain | W3C validator |