Theorem nfci 2883

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2880

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

This theorem depends on definitions:  df-bi 207  df-nfc 2882

This theorem is referenced by:  nfcii  2884  nfcv  2895  nfab1  2897  nfab  2901  nfabg  2902  nfaba1  2903  nfdif  4078  nfun  4119  nfin  4173  nfiu1  4979  iinabrex  32553  fpwrelmap  32722  esumfzf  34105  fsumiunss  45702  climsuse  45735  climinff  45738  fnlimfvre  45799  limsupre3uzlem  45860  pimdecfgtioc  46840  pimincfltioc  46841  smfmullem4  46919  smflimsupmpt  46954