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

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2884

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

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  4109  nfun  4150  nfin  4204  nfiu1  5008  iinabrex  32555  fpwrelmap  32715  esumfzf  34105  fsumiunss  45571  climsuse  45604  climinff  45607  fnlimfvre  45670  limsupre3uzlem  45731  pimdecfgtioc  46711  pimincfltioc  46712  smfmullem4  46790  smflimsupmpt  46825