Theorem nfci 2887

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

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

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 2886

This theorem is referenced by:  nfcii  2888  nfcv  2904  nfab1  2906  nfab  2910  nfabg  2911  iinabrex  31800  fpwrelmap  31958  esumfzf  33067  fsumiunss  44291  climsuse  44324  climinff  44327  fnlimfvre  44390  limsupre3uzlem  44451  pimdecfgtioc  45431  pimincfltioc  45432  smfmullem4  45510  smflimsupmpt  45545