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  4082  nfun  4123  nfin  4177  nfiu1  4980  iinabrex  32531  fpwrelmap  32689  esumfzf  34038  fsumiunss  45560  climsuse  45593  climinff  45596  fnlimfvre  45659  limsupre3uzlem  45720  pimdecfgtioc  46700  pimincfltioc  46701  smfmullem4  46779  smflimsupmpt  46814