Theorem nfcii 2888

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

Syntax hints:   → wi 4  ∀wal 1541   ∈ wcel 2110  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-10 2141

This theorem depends on definitions:  df-bi 210  df-ex 1788  df-nf 1792  df-nfc 2886

This theorem is referenced by:  bnj1316  32513  bnj1385  32525  bnj1400  32528  bnj1468  32539  bnj1534  32546  bnj1542  32550  bnj1228  32704  bnj1307  32716  bnj1448  32740  bnj1466  32746  bnj1463  32748  bnj1491  32750  bnj1312  32751  bnj1498  32754  bnj1520  32759  bnj1525  32762  bnj1529  32763  bnj1523  32764