Theorem nfci 2919

Description: Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfci.1	⊢ Ⅎ𝑥 𝑦 ∈ 𝐴

Assertion

Ref	Expression
nfci	⊢ Ⅎ𝑥𝐴

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfci

Step	Hyp	Ref	Expression
1		df-nfc 2918	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
2		nfci.1	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
3	1, 2	mpgbir 1826	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:  Ⅎwnf 1810   ∈ wcel 2149  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822

This theorem depends on definitions:  df-bi 210  df-nfc 2918

This theorem is referenced by:  nfcii  2920  nfcv  2931  nfab1  2933  nfab  2937  nfabg  2938  nfaba1  2939  nfdif  4092  nfun  4132  nfin  4185  nfiu1  4993  iinabrex  32851  fpwrelmap  33015  esumfzf  34400  fsumiunss  46176  climsuse  46209  climinff  46212  fnlimfvre  46273  limsupre3uzlem  46334  pimdecfgtioc  47314  pimincfltioc  47315  smfmullem4  47393  smflimsupmpt  47428