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

Theorem nfcii 2423
Description: Deduce that a class  A does not have  x free in it. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfcii.1  |-  ( y  e.  A  ->  A. x  y  e.  A )
Assertion
Ref Expression
nfcii  |-  F/_ x A
Distinct variable groups:    x, y    y, A
Allowed substitution hint:    A( x)

Proof of Theorem nfcii
StepHypRef Expression
1 nfcii.1 . . 3  |-  ( y  e.  A  ->  A. x  y  e.  A )
21nfi 1541 . 2  |-  F/ x  y  e.  A
32nfci 2422 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1530    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  gsumdixp  15408  bnj1316  29169  bnj1385  29181  bnj1400  29184  bnj1468  29194  bnj1534  29201  bnj1542  29205  bnj1228  29357  bnj1307  29369  bnj1311  29370  bnj1448  29393  bnj1466  29399  bnj1463  29401  bnj1491  29403  bnj1312  29404  bnj1498  29407  bnj1520  29412  bnj1525  29415  bnj1529  29416  bnj1523  29417
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536
This theorem depends on definitions:  df-bi 177  df-nf 1535  df-nfc 2421
  Copyright terms: Public domain W3C validator