Theorem nfci 2890

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2106  Ⅎwnfc 2887

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

This theorem depends on definitions:  df-bi 206  df-nfc 2889

This theorem is referenced by:  nfcii  2891  nfcv  2907  nfab1  2909  nfab  2913  nfabg  2914  iinabrex  30908  fpwrelmap  31068  esumfzf  32037  fsumiunss  43116  climsuse  43149  climinff  43152  fnlimfvre  43215  limsupre3uzlem  43276  pimdecfgtioc  44252  pimincfltioc  44253  smfmullem4  44328  smflimsupmpt  44362