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  4070  nfun  4111  nfin  4165  nfiu1  4970  iinabrex  32654  fpwrelmap  32821  esumfzf  34229  fsumiunss  46023  climsuse  46056  climinff  46059  fnlimfvre  46120  limsupre3uzlem  46181  pimdecfgtioc  47161  pimincfltioc  47162  smfmullem4  47240  smflimsupmpt  47275