Theorem nfcii 2882

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

Syntax hints:   → wi 4  ∀wal 1532   ∈ wcel 2099  Ⅎwnfc 2878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-10 2130

This theorem depends on definitions:  df-bi 206  df-ex 1775  df-nf 1779  df-nfc 2880

This theorem is referenced by:  bnj1316  34387  bnj1385  34399  bnj1400  34402  bnj1468  34413  bnj1534  34420  bnj1542  34424  bnj1228  34578  bnj1307  34590  bnj1448  34614  bnj1466  34620  bnj1463  34622  bnj1491  34624  bnj1312  34625  bnj1498  34628  bnj1520  34633  bnj1525  34636  bnj1529  34637  bnj1523  34638