Theorem nfcii 2784

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

Syntax hints:   → wi 4  ∀wal 1521   ∈ wcel 2030  Ⅎwnfc 2780

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-10 2059

This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-nfc 2782

This theorem is referenced by:  bnj1316  31017  bnj1385  31029  bnj1400  31032  bnj1468  31042  bnj1534  31049  bnj1542  31053  bnj1228  31205  bnj1307  31217  bnj1448  31241  bnj1466  31247  bnj1463  31249  bnj1491  31251  bnj1312  31252  bnj1498  31255  bnj1520  31260  bnj1525  31263  bnj1529  31264  bnj1523  31265