Theorem nfcii 2920

Description: Deduce that a class 𝐴 does not have 𝑥 free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)

Hypothesis

Ref	Expression
nfcii.1	⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)

Assertion

Ref	Expression
nfcii	⊢ Ⅎ𝑥𝐴

Distinct variable groups:   𝑥,𝑦   𝑦,𝐴

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem nfcii

Step	Hyp	Ref	Expression
1		nfcii.1	. . 3 ⊢ (𝑦 ∈ 𝐴 → ∀𝑥 𝑦 ∈ 𝐴)
2	1	nf5i 2187	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
3	2	nfci 2919	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   → wi 4  ∀wal 1565   ∈ wcel 2149  Ⅎwnfc 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-10 2182

This theorem depends on definitions:  df-bi 210  df-ex 1807  df-nf 1811  df-nfc 2918

This theorem is referenced by:  bnj1316  35149  bnj1385  35161  bnj1400  35164  bnj1468  35175  bnj1534  35182  bnj1542  35186  bnj1228  35340  bnj1307  35352  bnj1448  35376  bnj1466  35382  bnj1463  35384  bnj1491  35386  bnj1312  35387  bnj1498  35390  bnj1520  35395  bnj1525  35398  bnj1529  35399  bnj1523  35400