ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfi Unicode version

Theorem nfi 1396
Description: Deduce that  x is not free in  ph from the definition. (Contributed by Mario Carneiro, 11-Aug-2016.)
Hypothesis
Ref Expression
nfi.1  |-  ( ph  ->  A. x ph )
Assertion
Ref Expression
nfi  |-  F/ x ph

Proof of Theorem nfi
StepHypRef Expression
1 df-nf 1395 . 2  |-  ( F/ x ph  <->  A. x
( ph  ->  A. x ph ) )
2 nfi.1 . 2  |-  ( ph  ->  A. x ph )
31, 2mpgbir 1387 1  |-  F/ x ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287   F/wnf 1394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1383
This theorem depends on definitions:  df-bi 115  df-nf 1395
This theorem is referenced by:  nfth  1398  nfnth  1399  nfe1  1430  nfdh  1462  nfv  1466  nfa1  1479  nfan1  1501  nfim1  1508  nfor  1511  nfal  1513  nfex  1573  nfae  1654  cbv3h  1678  nfs1  1737  nfs1v  1863  hbsb  1871  sbco2h  1886  hbsbd  1906  dvelimALT  1934  dvelimfv  1935  hbeu  1969  hbeud  1970  eu3h  1993  mo3h  2001  nfsab1  2078  nfsab  2080  nfcii  2219  nfcri  2222
  Copyright terms: Public domain W3C validator