Theorem nfcii 2879

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

Syntax hints:   → wi 4  ∀wal 1531   ∈ wcel 2098  Ⅎwnfc 2875

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-10 2129

This theorem depends on definitions:  df-bi 206  df-ex 1774  df-nf 1778  df-nfc 2877

This theorem is referenced by:  bnj1316  34521  bnj1385  34533  bnj1400  34536  bnj1468  34547  bnj1534  34554  bnj1542  34558  bnj1228  34712  bnj1307  34724  bnj1448  34748  bnj1466  34754  bnj1463  34756  bnj1491  34758  bnj1312  34759  bnj1498  34762  bnj1520  34767  bnj1525  34770  bnj1529  34771  bnj1523  34772