Theorem nfcii 2891

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

Syntax hints:   → wi 4  ∀wal 1537   ∈ wcel 2106  Ⅎwnfc 2887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-10 2137

This theorem depends on definitions:  df-bi 206  df-ex 1783  df-nf 1787  df-nfc 2889

This theorem is referenced by:  bnj1316  32800  bnj1385  32812  bnj1400  32815  bnj1468  32826  bnj1534  32833  bnj1542  32837  bnj1228  32991  bnj1307  33003  bnj1448  33027  bnj1466  33033  bnj1463  33035  bnj1491  33037  bnj1312  33038  bnj1498  33041  bnj1520  33046  bnj1525  33049  bnj1529  33050  bnj1523  33051