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

Theorem nfcii 2410
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 1538 . 2  |-  F/ x  y  e.  A
32nfci 2409 1  |-  F/_ x A
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1527    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  gsumdixp  15392  bnj1316  28226  bnj1385  28238  bnj1400  28241  bnj1468  28251  bnj1534  28258  bnj1542  28262  bnj1228  28414  bnj1307  28426  bnj1311  28427  bnj1448  28450  bnj1466  28456  bnj1463  28458  bnj1491  28460  bnj1312  28461  bnj1498  28464  bnj1520  28469  bnj1525  28472  bnj1529  28473  bnj1523  28474
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533
This theorem depends on definitions:  df-bi 177  df-nf 1532  df-nfc 2408
  Copyright terms: Public domain W3C validator