Theorem nfcii 2916

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

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

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 2179

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

This theorem is used by:  bnj1316  35249  bnj1385  35261  bnj1400  35264  bnj1468  35275  bnj1534  35282  bnj1542  35286  bnj1228  35440  bnj1307  35452  bnj1448  35476  bnj1466  35482  bnj1463  35484  bnj1491  35486  bnj1312  35487  bnj1498  35490  bnj1520  35495  bnj1525  35498  bnj1529  35499  bnj1523  35500