Theorem nfcii 2883

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2111  Ⅎwnfc 2879

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-10 2144

This theorem depends on definitions:  df-bi 207  df-ex 1781  df-nf 1785  df-nfc 2881

This theorem is referenced by:  bnj1316  34830  bnj1385  34842  bnj1400  34845  bnj1468  34856  bnj1534  34863  bnj1542  34867  bnj1228  35021  bnj1307  35033  bnj1448  35057  bnj1466  35063  bnj1463  35065  bnj1491  35067  bnj1312  35068  bnj1498  35071  bnj1520  35076  bnj1525  35079  bnj1529  35080  bnj1523  35081