Theorem nfcii 2915

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

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

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 2180

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

This theorem is used by:  bnj1316  35561  bnj1385  35573  bnj1400  35576  bnj1468  35587  bnj1534  35594  bnj1542  35598  bnj1228  35752  bnj1307  35764  bnj1448  35788  bnj1466  35794  bnj1463  35796  bnj1491  35798  bnj1312  35799  bnj1498  35802  bnj1520  35807  bnj1525  35810  bnj1529  35811  bnj1523  35812