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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2114  Ⅎwnfc 2961

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 2145

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

This theorem is referenced by:  bnj1316  32092  bnj1385  32104  bnj1400  32107  bnj1468  32118  bnj1534  32125  bnj1542  32129  bnj1228  32283  bnj1307  32295  bnj1448  32319  bnj1466  32325  bnj1463  32327  bnj1491  32329  bnj1312  32330  bnj1498  32333  bnj1520  32338  bnj1525  32341  bnj1529  32342  bnj1523  32343