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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

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 207  df-nfc 2886

This theorem is referenced by:  nfcii  2888  nfcv  2899  nfab1  2901  nfab  2905  nfabg  2906  nfaba1  2907  nfdif  4083  nfun  4124  nfin  4178  nfiu1  4984  iinabrex  32655  fpwrelmap  32822  esumfzf  34246  fsumiunss  45932  climsuse  45965  climinff  45968  fnlimfvre  46029  limsupre3uzlem  46090  pimdecfgtioc  47070  pimincfltioc  47071  smfmullem4  47149  smflimsupmpt  47184