Theorem nfcii 2912

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1568   ∈ wcel 2145  Ⅎwnfc 2908

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-10 2178

This proof depends on definitions:  df-bi 210  df-ex 1813  df-nf 1817  df-nfc 2910

This theorem is used by:  bnj1316  35450  bnj1385  35462  bnj1400  35465  bnj1468  35476  bnj1534  35483  bnj1542  35487  bnj1228  35641  bnj1307  35653  bnj1448  35677  bnj1466  35683  bnj1463  35685  bnj1491  35687  bnj1312  35688  bnj1498  35691  bnj1520  35696  bnj1525  35699  bnj1529  35700  bnj1523  35701