Theorem nfcii 2887

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

Syntax hints:   → wi 4  ∀wal 1539   ∈ wcel 2113  Ⅎwnfc 2883

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 2146

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

This theorem is referenced by:  bnj1316  34976  bnj1385  34988  bnj1400  34991  bnj1468  35002  bnj1534  35009  bnj1542  35013  bnj1228  35167  bnj1307  35179  bnj1448  35203  bnj1466  35209  bnj1463  35211  bnj1491  35213  bnj1312  35214  bnj1498  35217  bnj1520  35222  bnj1525  35225  bnj1529  35226  bnj1523  35227