Theorem nfci 2889

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

Syntax hints:  Ⅎwnf 1790   ∈ wcel 2119  Ⅎwnfc 2886

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

This theorem depends on definitions:  df-bi 208  df-nfc 2888

This theorem is referenced by:  nfcii  2890  nfcv  2901  nfab1  2903  nfab  2907  nfabg  2908  nfaba1  2909  nfdif  4060  nfun  4100  nfin  4153  nfiu1  4957  iinabrex  32658  fpwrelmap  32825  esumfzf  34253  fsumiunss  46020  climsuse  46053  climinff  46056  fnlimfvre  46117  limsupre3uzlem  46178  pimdecfgtioc  47158  pimincfltioc  47159  smfmullem4  47237  smflimsupmpt  47272