Theorem nfci 2882

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2111  Ⅎwnfc 2879

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 2881

This theorem is referenced by:  nfcii  2883  nfcv  2894  nfab1  2896  nfab  2900  nfabg  2901  nfaba1  2902  nfdif  4079  nfun  4120  nfin  4174  nfiu1  4977  iinabrex  32547  fpwrelmap  32714  esumfzf  34080  fsumiunss  45621  climsuse  45654  climinff  45657  fnlimfvre  45718  limsupre3uzlem  45779  pimdecfgtioc  46759  pimincfltioc  46760  smfmullem4  46838  smflimsupmpt  46873