Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfcii Structured version   Visualization version   GIF version

Theorem nfcii 2784
 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
StepHypRef Expression
1 nfcii.1 . . 3 (𝑦𝐴 → ∀𝑥 𝑦𝐴)
21nf5i 2064 . 2 𝑥 𝑦𝐴
32nfci 2783 1 𝑥𝐴
 Colors of variables: wff setvar class Syntax hints:   → wi 4  ∀wal 1521   ∈ wcel 2030  Ⅎwnfc 2780 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-10 2059 This theorem depends on definitions:  df-bi 197  df-ex 1745  df-nf 1750  df-nfc 2782 This theorem is referenced by:  bnj1316  31017  bnj1385  31029  bnj1400  31032  bnj1468  31042  bnj1534  31049  bnj1542  31053  bnj1228  31205  bnj1307  31217  bnj1448  31241  bnj1466  31247  bnj1463  31249  bnj1491  31251  bnj1312  31252  bnj1498  31255  bnj1520  31260  bnj1525  31263  bnj1529  31264  bnj1523  31265
 Copyright terms: Public domain W3C validator