Theorem nfcii 2892

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2106  Ⅎwnfc 2888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-10 2139

This theorem depends on definitions:  df-bi 207  df-ex 1777  df-nf 1781  df-nfc 2890

This theorem is referenced by:  bnj1316  34813  bnj1385  34825  bnj1400  34828  bnj1468  34839  bnj1534  34846  bnj1542  34850  bnj1228  35004  bnj1307  35016  bnj1448  35040  bnj1466  35046  bnj1463  35048  bnj1491  35050  bnj1312  35051  bnj1498  35054  bnj1520  35059  bnj1525  35062  bnj1529  35063  bnj1523  35064