Theorem nfci 2886

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 2885	. 2 ⊢ (Ⅎ𝑥𝐴 ↔ ∀𝑦Ⅎ𝑥 𝑦 ∈ 𝐴)
2		nfci.1	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
3	1, 2	mpgbir 1801	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2883

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

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  4069  nfun  4110  nfin  4164  nfiu1  4969  iinabrex  32639  fpwrelmap  32806  esumfzf  34213  fsumiunss  46005  climsuse  46038  climinff  46041  fnlimfvre  46102  limsupre3uzlem  46163  pimdecfgtioc  47143  pimincfltioc  47144  smfmullem4  47222  smflimsupmpt  47257