Theorem nfcii 2893

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2107  Ⅎwnfc 2889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-10 2140

This theorem depends on definitions:  df-bi 207  df-ex 1779  df-nf 1783  df-nfc 2891

This theorem is referenced by:  bnj1316  34835  bnj1385  34847  bnj1400  34850  bnj1468  34861  bnj1534  34868  bnj1542  34872  bnj1228  35026  bnj1307  35038  bnj1448  35062  bnj1466  35068  bnj1463  35070  bnj1491  35072  bnj1312  35073  bnj1498  35076  bnj1520  35081  bnj1525  35084  bnj1529  35085  bnj1523  35086