Theorem nfci 2913

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

Syntax hints:  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

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

This theorem depends on definitions:  df-bi 210  df-nfc 2912

This theorem is referenced by:  nfcii  2914  nfcv  2925  nfab1  2927  nfab  2931  nfabg  2932  nfaba1  2933  nfdif  4084  nfun  4124  nfin  4177  nfiu1  4992  iinabrex  32914  fpwrelmap  33078  esumfzf  34459  fsumiunss  46291  climsuse  46324  climinff  46327  fnlimfvre  46388  limsupre3uzlem  46449  pimdecfgtioc  47429  pimincfltioc  47430  smfmullem4  47508  smflimsupmpt  47543