Theorem nfci 2966

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2963

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 209  df-nfc 2965

This theorem is referenced by:  nfcii  2967  nfcv  2979  nfab1  2981  nfab  2986  nfabg  2987  fpwrelmap  30471  esumfzf  31330  fsumiunss  41863  climsuse  41896  climinff  41899  fnlimfvre  41962  limsupre3uzlem  42023  pimdecfgtioc  43000  pimincfltioc  43001  smfmullem4  43076  smflimsupmpt  43110