Theorem nfcii 2912

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

Syntax hints:   → wi 4  ∀wal 1557   ∈ wcel 2141  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-10 2174

This theorem depends on definitions:  df-bi 209  df-ex 1799  df-nf 1803  df-nfc 2910

This theorem is referenced by:  bnj1316  35076  bnj1385  35088  bnj1400  35091  bnj1468  35102  bnj1534  35109  bnj1542  35113  bnj1228  35267  bnj1307  35279  bnj1448  35303  bnj1466  35309  bnj1463  35311  bnj1491  35313  bnj1312  35314  bnj1498  35317  bnj1520  35322  bnj1525  35325  bnj1529  35326  bnj1523  35327