Theorem nfci 2891

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

Syntax hints:  Ⅎwnf 1780   ∈ wcel 2106  Ⅎwnfc 2888

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

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

This theorem is referenced by:  nfcii  2892  nfcv  2903  nfab1  2905  nfab  2909  nfabg  2910  nfaba1  2911  nfdif  4139  nfun  4180  nfin  4232  nfiu1  5032  iinabrex  32589  fpwrelmap  32751  esumfzf  34050  fsumiunss  45531  climsuse  45564  climinff  45567  fnlimfvre  45630  limsupre3uzlem  45691  pimdecfgtioc  46671  pimincfltioc  46672  smfmullem4  46750  smflimsupmpt  46785