Theorem nfcii 2897

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

Syntax hints:   → wi 4  ∀wal 1535   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-10 2141

This theorem depends on definitions:  df-bi 207  df-ex 1778  df-nf 1782  df-nfc 2895

This theorem is referenced by:  bnj1316  34796  bnj1385  34808  bnj1400  34811  bnj1468  34822  bnj1534  34829  bnj1542  34833  bnj1228  34987  bnj1307  34999  bnj1448  35023  bnj1466  35029  bnj1463  35031  bnj1491  35033  bnj1312  35034  bnj1498  35037  bnj1520  35042  bnj1525  35045  bnj1529  35046  bnj1523  35047