Theorem nfci 2892

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

Syntax hints:  Ⅎwnf 1782   ∈ wcel 2107  Ⅎwnfc 2889

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

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

This theorem is referenced by:  nfcii  2893  nfcv  2904  nfab1  2906  nfab  2910  nfabg  2911  nfaba1  2912  nfdif  4128  nfun  4169  nfin  4223  nfiu1  5026  iinabrex  32583  fpwrelmap  32745  esumfzf  34071  fsumiunss  45595  climsuse  45628  climinff  45631  fnlimfvre  45694  limsupre3uzlem  45755  pimdecfgtioc  46735  pimincfltioc  46736  smfmullem4  46814  smflimsupmpt  46849