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 1818	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:  Ⅎwnf 1802   ∈ wcel 2141  Ⅎwnfc 2908

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

This theorem depends on definitions:  df-bi 209  df-nfc 2910

This theorem is referenced by:  nfcii  2912  nfcv  2923  nfab1  2925  nfab  2929  nfabg  2930  nfaba1  2931  nfdif  4081  nfun  4121  nfin  4174  nfiu1  4982  iinabrex  32729  fpwrelmap  32896  esumfzf  34327  fsumiunss  46112  climsuse  46145  climinff  46148  fnlimfvre  46209  limsupre3uzlem  46270  pimdecfgtioc  47250  pimincfltioc  47251  smfmullem4  47329  smflimsupmpt  47364