Theorem nfci 2880

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

Syntax hints:  Ⅎwnf 1791   ∈ wcel 2112  Ⅎwnfc 2877

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

This theorem depends on definitions:  df-bi 210  df-nfc 2879

This theorem is referenced by:  nfcii  2881  nfcv  2897  nfab1  2899  nfab  2903  nfabg  2904  iinabrex  30581  fpwrelmap  30742  esumfzf  31703  fsumiunss  42734  climsuse  42767  climinff  42770  fnlimfvre  42833  limsupre3uzlem  42894  pimdecfgtioc  43867  pimincfltioc  43868  smfmullem4  43943  smflimsupmpt  43977