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

Theorem nfra1 2349
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 2305 . 2 (x A φx(x Aφ))
2 nfa1 1431 . 2 xx(x Aφ)
31, 2nfxfr 1360 1 xx A φ
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1240  wnf 1346   wcel 1390  wral 2300
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 1333  ax-gen 1335  ax-ial 1424
This theorem depends on definitions:  df-bi 110  df-nf 1347  df-ral 2305
This theorem is referenced by:  nfra2xy  2358  r19.12  2416  ralbi  2439  rexbi  2440  nfss  2932  ralidm  3315  nfii1  3678  dfiun2g  3679  mpteq12f  3827  reusv1  4155  ralxfrALT  4164  peano2  4260  fun11iun  5088  fvmptssdm  5196  ffnfv  5264  riota5f  5432  mpt2eq123  5503  tfri3  5891  indstr  8261  bj-rspgt  8859
  Copyright terms: Public domain W3C validator