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 2106  Ⅎ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 206  df-nfc 2885

This theorem is referenced by:  nfcii  2887  nfcv  2903  nfab1  2905  nfab  2909  nfabg  2910  iinabrex  31729  fpwrelmap  31893  esumfzf  32962  fsumiunss  44128  climsuse  44161  climinff  44164  fnlimfvre  44227  limsupre3uzlem  44288  pimdecfgtioc  45268  pimincfltioc  45269  smfmullem4  45347  smflimsupmpt  45382