Theorem nfcii 2935

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

Syntax hints:   → wi 4  ∀wal 1518   ∈ wcel 2079  Ⅎwnfc 2931

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

This theorem depends on definitions:  df-bi 208  df-ex 1760  df-nf 1764  df-nfc 2933

This theorem is referenced by:  bnj1316  31665  bnj1385  31677  bnj1400  31680  bnj1468  31690  bnj1534  31697  bnj1542  31701  bnj1228  31853  bnj1307  31865  bnj1448  31889  bnj1466  31895  bnj1463  31897  bnj1491  31899  bnj1312  31900  bnj1498  31903  bnj1520  31908  bnj1525  31911  bnj1529  31912  bnj1523  31913