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  4996  iinabrex  32855  fpwrelmap  33019  esumfzf  34404  fsumiunss  46217  climsuse  46250  climinff  46253  fnlimfvre  46314  limsupre3uzlem  46375  pimdecfgtioc  47355  pimincfltioc  47356  smfmullem4  47434  smflimsupmpt  47469