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

Theorem nfra1 2409
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 2364 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1479 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1408 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1287   F/wnf 1394    e. wcel 1438   A.wral 2359
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-5 1381  ax-gen 1383  ax-ial 1472
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  nfra2xy  2418  r19.12  2478  ralbi  2501  rexbi  2502  nfss  3016  ralidm  3378  nfii1  3756  dfiun2g  3757  mpteq12f  3910  reusv1  4271  ralxfrALT  4280  peano2  4400  fun11iun  5258  fvmptssdm  5371  ffnfv  5440  riota5f  5614  mpt2eq123  5690  tfri3  6114  nneneq  6553  exmidomni  6777  caucvgsrlemgt1  7319  lble  8380  indstr  9050  fimaxre2  10622  zsupcllemstep  11034  bezoutlemmain  11080  bezoutlemzz  11084  bj-rspgt  11343
  Copyright terms: Public domain W3C validator