Theorem nfcii 2887

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2106  Ⅎwnfc 2883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-ex 1782  df-nf 1786  df-nfc 2885

This theorem is referenced by:  bnj1316  33726  bnj1385  33738  bnj1400  33741  bnj1468  33752  bnj1534  33759  bnj1542  33763  bnj1228  33917  bnj1307  33929  bnj1448  33953  bnj1466  33959  bnj1463  33961  bnj1491  33963  bnj1312  33964  bnj1498  33967  bnj1520  33972  bnj1525  33975  bnj1529  33976  bnj1523  33977