Theorem nfci 2910

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

This proof depends on syntax axioms:  Ⅎwnf 1815   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827

This proof depends on definitions:  df-bi 210  df-nfc 2909

This theorem is used by:  nfcii  2911  nfcv  2922  nfab1  2924  nfab  2928  nfabg  2929  nfaba1  2930  nfdif  4065  nfin  4120  nfun  4168  nfiu1  4985  iinabrex  33214  fpwrelmap  33375  esumfzf  34751  fsumiunss  46695  climsuse  46728  climinff  46731  fnlimfvre  46792  limsupre3uzlem  46853  pimdecfgtioc  47833  pimincfltioc  47834  smfmullem4  47912  smflimsupmpt  47947