| 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 2881 | . 2 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴) | |
| 2 | nfci.1 | . 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴 | |
| 3 | 1, 2 | mpgbir 1800 | 1 ⊢ Ⅎ𝑥𝐴 |
| Colors of variables: wff setvar class |
| Syntax hints: Ⅎwnf 1784 ∈ wcel 2111 Ⅎwnfc 2879 |
| 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 2881 |
| This theorem is referenced by: nfcii 2883 nfcv 2894 nfab1 2896 nfab 2900 nfabg 2901 nfaba1 2902 nfdif 4076 nfun 4117 nfin 4171 nfiu1 4975 iinabrex 32549 fpwrelmap 32716 esumfzf 34082 fsumiunss 45674 climsuse 45707 climinff 45710 fnlimfvre 45771 limsupre3uzlem 45832 pimdecfgtioc 46812 pimincfltioc 46813 smfmullem4 46891 smflimsupmpt 46926 |
| Copyright terms: Public domain | W3C validator |