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 1800	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2883

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 2885

This theorem is referenced by:  nfcii  2887  nfcv  2898  nfab1  2900  nfab  2904  nfabg  2905  nfaba1  2906  nfdif  4081  nfun  4122  nfin  4176  nfiu1  4982  iinabrex  32644  fpwrelmap  32812  esumfzf  34226  fsumiunss  45821  climsuse  45854  climinff  45857  fnlimfvre  45918  limsupre3uzlem  45979  pimdecfgtioc  46959  pimincfltioc  46960  smfmullem4  47038  smflimsupmpt  47073