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  34117  bnj1385  34129  bnj1400  34132  bnj1468  34143  bnj1534  34150  bnj1542  34154  bnj1228  34308  bnj1307  34320  bnj1448  34344  bnj1466  34350  bnj1463  34352  bnj1491  34354  bnj1312  34355  bnj1498  34358  bnj1520  34363  bnj1525  34366  bnj1529  34367  bnj1523  34368