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  3679  dfiun2g  3680  mpteq12f  3828  reusv1  4156  ralxfrALT  4165  peano2  4261  fun11iun  5090  fvmptssdm  5198  ffnfv  5266  riota5f  5435  mpt2eq123  5506  tfri3  5894  indstr  8312  bj-rspgt  9260
  Copyright terms: Public domain W3C validator