Theorem nfcii 2911

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1567   ∈ wcel 2144  Ⅎwnfc 2907

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-10 2177

This proof depends on definitions:  df-bi 210  df-ex 1812  df-nf 1816  df-nfc 2909

This theorem is used by:  bnj1316  35500  bnj1385  35512  bnj1400  35515  bnj1468  35526  bnj1534  35533  bnj1542  35537  bnj1228  35691  bnj1307  35703  bnj1448  35727  bnj1466  35733  bnj1463  35735  bnj1491  35737  bnj1312  35738  bnj1498  35741  bnj1520  35746  bnj1525  35749  bnj1529  35750  bnj1523  35751