Theorem nfci 2885

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2106  Ⅎwnfc 2882

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

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

This theorem is referenced by:  nfcii  2886  nfcv  2902  nfab1  2904  nfab  2908  nfabg  2909  iinabrex  31660  fpwrelmap  31824  esumfzf  32882  fsumiunss  44050  climsuse  44083  climinff  44086  fnlimfvre  44149  limsupre3uzlem  44210  pimdecfgtioc  45190  pimincfltioc  45191  smfmullem4  45269  smflimsupmpt  45304