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 2960 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
2 | nfci.1 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | |
3 | 1, 2 | mpgbir 1791 | 1 ⊢ Ⅎ𝑥𝐴 |
Colors of variables: wff setvar class |
Syntax hints: Ⅎwnf 1775 ∈ wcel 2105 Ⅎwnfc 2958 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 |
This theorem depends on definitions: df-bi 208 df-nfc 2960 |
This theorem is referenced by: nfcii 2962 nfcv 2974 nfab1 2976 nfab 2981 nfabg 2982 fpwrelmap 30395 esumfzf 31227 fsumiunss 41732 climsuse 41765 climinff 41768 fnlimfvre 41831 limsupre3uzlem 41892 pimdecfgtioc 42870 pimincfltioc 42871 smfmullem4 42946 smflimsupmpt 42980 |
Copyright terms: Public domain | W3C validator |