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

Theorem nfra1 2420
Description: 𝑥 is not free in 𝑥𝐴𝜑. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)
Assertion
Ref Expression
nfra1 𝑥𝑥𝐴 𝜑

Proof of Theorem nfra1
StepHypRef Expression
1 df-ral 2375 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1486 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1415 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1294  wnf 1401  wcel 1445  wral 2370
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ial 1479
This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375
This theorem is referenced by:  nfra2xy  2429  r19.12  2491  ralbi  2515  rexbi  2516  nfss  3032  ralidm  3402  nfii1  3783  dfiun2g  3784  mpteq12f  3940  reusv1  4308  ralxfrALT  4317  peano2  4438  fun11iun  5309  fvmptssdm  5423  ffnfv  5495  riota5f  5670  mpt2eq123  5746  tfri3  6170  nfixp1  6515  nneneq  6653  exmidomni  6885  mkvprop  6901  caucvgsrlemgt1  7437  lble  8505  indstr  9180  fimaxre2  10773  zsupcllemstep  11368  bezoutlemmain  11414  bezoutlemzz  11418  mulcncf  12354  bj-rspgt  12394
  Copyright terms: Public domain W3C validator