Theorem nfcii 2965

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

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2110  Ⅎwnfc 2961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-10 2141

This theorem depends on definitions:  df-bi 209  df-ex 1777  df-nf 1781  df-nfc 2963

This theorem is referenced by:  bnj1316  32087  bnj1385  32099  bnj1400  32102  bnj1468  32113  bnj1534  32120  bnj1542  32124  bnj1228  32278  bnj1307  32290  bnj1448  32314  bnj1466  32320  bnj1463  32322  bnj1491  32324  bnj1312  32325  bnj1498  32328  bnj1520  32333  bnj1525  32336  bnj1529  32337  bnj1523  32338