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

Syntax hints:   → wi 4  ∀wal 1538   ∈ wcel 2109  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-10 2142

This theorem depends on definitions:  df-bi 207  df-ex 1780  df-nf 1784  df-nfc 2886

This theorem is referenced by:  bnj1316  34856  bnj1385  34868  bnj1400  34871  bnj1468  34882  bnj1534  34889  bnj1542  34893  bnj1228  35047  bnj1307  35059  bnj1448  35083  bnj1466  35089  bnj1463  35091  bnj1491  35093  bnj1312  35094  bnj1498  35097  bnj1520  35102  bnj1525  35105  bnj1529  35106  bnj1523  35107