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

Theorem nfra1 2333
Description: x is not free in x Aφ. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1 xx A φ

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2289 . 2 (x A φx(x Aφ))
2 nfa1 1416 . 2 xx(x Aφ)
31, 2nfxfr 1343 1 xx A φ
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1226  wnf 1329   wcel 1374  wral 2284
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-gen 1318  ax-ial 1409
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-ral 2289
This theorem is referenced by:  nfra2xy  2342  r19.12  2400  ralbi  2423  rexbi  2424  nfss  2915  ralidm  3300  nfii1  3662  dfiun2g  3663  mpteq12f  3811  reusv1  4140  ralxfrALT  4149  peano2  4245  fun11iun  5072  fvmptssdm  5180  ffnfv  5248  riota5f  5416  mpt2eq123  5487  tfri3  5875  bj-rspgt  7032
  Copyright terms: Public domain W3C validator