Theorem nfci 2879

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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

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

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

This theorem is referenced by:  nfcii  2880  nfcv  2891  nfab1  2893  nfab  2897  nfabg  2898  nfaba1  2899  nfdif  4092  nfun  4133  nfin  4187  nfiu1  4991  iinabrex  32498  fpwrelmap  32656  esumfzf  34059  fsumiunss  45573  climsuse  45606  climinff  45609  fnlimfvre  45672  limsupre3uzlem  45733  pimdecfgtioc  46713  pimincfltioc  46714  smfmullem4  46792  smflimsupmpt  46827