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

Theorem nfra1 2372
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 2328 . 2  |-  ( A. x  e.  A  ph  <->  A. x
( x  e.  A  ->  ph ) )
2 nfa1 1450 . 2  |-  F/ x A. x ( x  e.  A  ->  ph )
31, 2nfxfr 1379 1  |-  F/ x A. x  e.  A  ph
Colors of variables: wff set class
Syntax hints:    -> wi 4   A.wal 1257   F/wnf 1365    e. wcel 1409   A.wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328
This theorem is referenced by:  nfra2xy  2381  r19.12  2439  ralbi  2462  rexbi  2463  nfss  2965  ralidm  3348  nfii1  3715  dfiun2g  3716  mpteq12f  3864  reusv1  4217  ralxfrALT  4226  peano2  4345  fun11iun  5174  fvmptssdm  5282  ffnfv  5350  riota5f  5519  mpt2eq123  5591  tfri3  5983  nneneq  6350  caucvgsrlemgt1  6936  indstr  8631  bj-rspgt  10291
  Copyright terms: Public domain W3C validator