| 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 1800 | 1 ⊢ Ⅎ𝑥𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: Ⅎwnf 1784 ∈ wcel 2113 Ⅎwnfc 2883 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 |
| This theorem depends on definitions: df-bi 207 df-nfc 2885 |
| This theorem is referenced by: nfcii 2887 nfcv 2898 nfab1 2900 nfab 2904 nfabg 2905 nfaba1 2906 nfdif 4081 nfun 4122 nfin 4176 nfiu1 4982 iinabrex 32644 fpwrelmap 32812 esumfzf 34226 fsumiunss 45821 climsuse 45854 climinff 45857 fnlimfvre 45918 limsupre3uzlem 45979 pimdecfgtioc 46959 pimincfltioc 46960 smfmullem4 47038 smflimsupmpt 47073 |
| Copyright terms: Public domain | W3C validator |