NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  nfra1 GIF version

Theorem nfra1 2664
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 2619 . 2 (x A φx(x Aφ))
2 nfa1 1788 . 2 xx(x Aφ)
31, 2nfxfr 1570 1 xx A φ
Colors of variables: wff setvar class
Syntax hints:  wi 4  wal 1540  wnf 1544   wcel 1710  wral 2614
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-11 1746
This theorem depends on definitions:  df-bi 177  df-ex 1542  df-nf 1545  df-ral 2619
This theorem is referenced by:  nfra2  2668  r19.12  2727  ralbi  2750  ralcom2  2775  nfss  3266  ralidm  3653  nfii1  3998  dfiun2g  3999  ncfinraise  4481  fun11iun  5305  chfnrn  5399  ffnfv  5427  mpteq12f  5655  mpt2eq123  5661  fvmptss  5705
  Copyright terms: Public domain W3C validator