Theorem nfci 2896

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

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

This theorem depends on definitions:  df-bi 207  df-nfc 2895

This theorem is referenced by:  nfcii  2897  nfcv  2908  nfab1  2910  nfab  2914  nfabg  2915  nfaba1  2916  nfdif  4152  nfun  4193  nfin  4245  nfiu1  5050  iinabrex  32591  fpwrelmap  32747  esumfzf  34033  fsumiunss  45496  climsuse  45529  climinff  45532  fnlimfvre  45595  limsupre3uzlem  45656  pimdecfgtioc  46636  pimincfltioc  46637  smfmullem4  46715  smflimsupmpt  46750