Theorem nfcii 2755

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

Syntax hints:   → wi 4  ∀wal 1481   ∈ wcel 1990  Ⅎwnfc 2751

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-10 2019

This theorem depends on definitions:  df-bi 197  df-ex 1705  df-nf 1710  df-nfc 2753

This theorem is referenced by:  bnj1316  30891  bnj1385  30903  bnj1400  30906  bnj1468  30916  bnj1534  30923  bnj1542  30927  bnj1228  31079  bnj1307  31091  bnj1448  31115  bnj1466  31121  bnj1463  31123  bnj1491  31125  bnj1312  31126  bnj1498  31129  bnj1520  31134  bnj1525  31137  bnj1529  31138  bnj1523  31139