Theorem nfcii 2742

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

Syntax hints:   → wi 4  ∀wal 1473   ∈ wcel 1977  Ⅎwnfc 2738

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-10 2006

This theorem depends on definitions:  df-bi 196  df-ex 1696  df-nf 1701  df-nfc 2740

This theorem is referenced by:  bnj1316  30145  bnj1385  30157  bnj1400  30160  bnj1468  30170  bnj1534  30177  bnj1542  30181  bnj1228  30333  bnj1307  30345  bnj1448  30369  bnj1466  30375  bnj1463  30377  bnj1491  30379  bnj1312  30380  bnj1498  30383  bnj1520  30388  bnj1525  30391  bnj1529  30392  bnj1523  30393