Theorem nfci 2915

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2146  Ⅎwnfc 2912

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 2914

This theorem is used by:  nfcii  2916  nfcv  2927  nfab1  2929  nfab  2933  nfabg  2934  nfaba1  2935  nfdif  4084  nfun  4124  nfin  4177  nfiu1  4994  iinabrex  32961  fpwrelmap  33124  esumfzf  34499  fsumiunss  46324  climsuse  46357  climinff  46360  fnlimfvre  46421  limsupre3uzlem  46482  pimdecfgtioc  47462  pimincfltioc  47463  smfmullem4  47541  smflimsupmpt  47576