Theorem nfcii 2890

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

Syntax hints:   → wi 4  ∀wal 1545   ∈ wcel 2119  Ⅎwnfc 2886

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-10 2152

This theorem depends on definitions:  df-bi 208  df-ex 1787  df-nf 1791  df-nfc 2888

This theorem is referenced by:  bnj1316  35002  bnj1385  35014  bnj1400  35017  bnj1468  35028  bnj1534  35035  bnj1542  35039  bnj1228  35193  bnj1307  35205  bnj1448  35229  bnj1466  35235  bnj1463  35237  bnj1491  35239  bnj1312  35240  bnj1498  35243  bnj1520  35248  bnj1525  35251  bnj1529  35252  bnj1523  35253