Theorem nfcii 2914

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 2181	. 2 ⊢ Ⅎ𝑥 𝑦 ∈ 𝐴
3	2	nfci 2913	1 ⊢ Ⅎ𝑥𝐴

Syntax hints:   → wi 4  ∀wal 1568   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-10 2176

This theorem depends on definitions:  df-bi 210  df-ex 1810  df-nf 1814  df-nfc 2912

This theorem is referenced by:  bnj1316  35208  bnj1385  35220  bnj1400  35223  bnj1468  35234  bnj1534  35241  bnj1542  35245  bnj1228  35399  bnj1307  35411  bnj1448  35435  bnj1466  35441  bnj1463  35443  bnj1491  35445  bnj1312  35446  bnj1498  35449  bnj1520  35454  bnj1525  35457  bnj1529  35458  bnj1523  35459