Theorem nfci 2911

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

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

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 2910

This theorem is used by:  nfcii  2912  nfcv  2923  nfab1  2925  nfab  2929  nfabg  2930  nfaba1  2931  nfdif  4077  nfun  4117  nfin  4170  nfiu1  4986  iinabrex  33156  fpwrelmap  33318  esumfzf  34694  fsumiunss  46556  climsuse  46589  climinff  46592  fnlimfvre  46653  limsupre3uzlem  46714  pimdecfgtioc  47694  pimincfltioc  47695  smfmullem4  47773  smflimsupmpt  47808