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

Theorem nfcii 2595
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 1610 . 2  |-  F/ x  y  e.  A
32nfci 2594 1  |-  F/_ x A
Colors of variables: wff setvar class
Syntax hints:    -> wi 4   A.wal 1381    e. wcel 1804   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605
This theorem depends on definitions:  df-bi 185  df-nf 1604  df-nfc 2593
This theorem is referenced by:  bnj1316  33747  bnj1385  33759  bnj1400  33762  bnj1468  33772  bnj1534  33779  bnj1542  33783  bnj1228  33935  bnj1307  33947  bnj1448  33971  bnj1466  33977  bnj1463  33979  bnj1491  33981  bnj1312  33982  bnj1498  33985  bnj1520  33990  bnj1525  33993  bnj1529  33994  bnj1523  33995
  Copyright terms: Public domain W3C validator