Theorem nfci 2910

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2145  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828

This proof depends on definitions:  df-bi 210  df-nfc 2909

This theorem is used by:  nfcii  2911  nfcv  2922  nfab1  2924  nfab  2928  nfabg  2929  nfaba1  2930  nfdif  4077  nfun  4117  nfin  4170  nfiu1  4986  iinabrex  33042  fpwrelmap  33204  esumfzf  34579  fsumiunss  46405  climsuse  46438  climinff  46441  fnlimfvre  46502  limsupre3uzlem  46563  pimdecfgtioc  47543  pimincfltioc  47544  smfmullem4  47622  smflimsupmpt  47657