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

Syntax hints:  Ⅎwnf 1787   ∈ wcel 2108  Ⅎwnfc 2886

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

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

This theorem is referenced by:  nfcii  2890  nfcv  2906  nfab1  2908  nfab  2912  nfabg  2913  iinabrex  30809  fpwrelmap  30970  esumfzf  31937  fsumiunss  43006  climsuse  43039  climinff  43042  fnlimfvre  43105  limsupre3uzlem  43166  pimdecfgtioc  44139  pimincfltioc  44140  smfmullem4  44215  smflimsupmpt  44249