Theorem nfci 2882

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

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