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

Theorem nfra1 2441
Description:  x is not free in  A. x  e.  A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1  |-  F/ x A. x  e.  A  ph

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2396 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1504 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1433 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1312   F/wnf 1419    e. wcel 1463   A.wral 2391
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-gen 1408  ax-ial 1497
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  nfra2xy  2450  r19.12  2513  ralbi  2539  rexbi  2540  nfss  3058  ralidm  3431  nfii1  3812  dfiun2g  3813  mpteq12f  3976  reusv1  4347  ralxfrALT  4356  peano2  4477  fun11iun  5354  fvmptssdm  5471  ffnfv  5544  riota5f  5720  mpoeq123  5796  tfri3  6230  nfixp1  6578  nneneq  6717  exmidomni  6980  mkvprop  6998  caucvgsrlemgt1  7567  suplocsrlem  7580  lble  8662  indstr  9337  fimaxre2  10938  zsupcllemstep  11534  bezoutlemmain  11582  bezoutlemzz  11586  exmidunben  11834  mulcncf  12655  limccnp2cntop  12698  bj-rspgt  12804  isomninnlem  13036
  Copyright terms: Public domain W3C validator