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

Syntax hints:   → wi 4  ∀wal 1540   ∈ wcel 2114  Ⅎ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 2147

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

This theorem is referenced by:  bnj1316  34962  bnj1385  34974  bnj1400  34977  bnj1468  34988  bnj1534  34995  bnj1542  34999  bnj1228  35153  bnj1307  35165  bnj1448  35189  bnj1466  35195  bnj1463  35197  bnj1491  35199  bnj1312  35200  bnj1498  35203  bnj1520  35208  bnj1525  35211  bnj1529  35212  bnj1523  35213