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

Theorem nfcii 2603
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 1682 . 2  |-  F/ x  y  e.  A
32nfci 2602 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1450    e. wcel 1904   F/_wnfc 2599
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677
This theorem depends on definitions:  df-bi 190  df-nf 1676  df-nfc 2601
This theorem is referenced by:  bnj1316  29704  bnj1385  29716  bnj1400  29719  bnj1468  29729  bnj1534  29736  bnj1542  29740  bnj1228  29892  bnj1307  29904  bnj1448  29928  bnj1466  29934  bnj1463  29936  bnj1491  29938  bnj1312  29939  bnj1498  29942  bnj1520  29947  bnj1525  29950  bnj1529  29951  bnj1523  29952
  Copyright terms: Public domain W3C validator