Theorem nfci 2914

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

This proof depends on syntax axioms:  Ⅎwnf 1816   ∈ wcel 2147  Ⅎwnfc 2911

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

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

This theorem is used by:  nfcii  2915  nfcv  2926  nfab1  2928  nfab  2932  nfabg  2933  nfaba1  2934  nfdif  4069  nfin  4124  nfun  4172  nfiu1  4991  iinabrex  33261  fpwrelmap  33421  esumfzf  34812  fsumiunss  46860  climsuse  46893  climinff  46896  fnlimfvre  46957  limsupre3uzlem  47018  pimdecfgtioc  47998  pimincfltioc  47999  smfmullem4  48077  smflimsupmpt  48112