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

Theorem nfra1 2372
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 2328 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1450 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1379 1 𝑥𝑥𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wi 4  wal 1257  wnf 1365  wcel 1409  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-ial 1443
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-ral 2328
This theorem is referenced by:  nfra2xy  2381  r19.12  2439  ralbi  2462  rexbi  2463  nfss  2966  ralidm  3349  nfii1  3716  dfiun2g  3717  mpteq12f  3865  reusv1  4218  ralxfrALT  4227  peano2  4346  fun11iun  5175  fvmptssdm  5283  ffnfv  5351  riota5f  5520  mpt2eq123  5592  tfri3  5984  nneneq  6351  caucvgsrlemgt1  6937  indstr  8632  bj-rspgt  10312
  Copyright terms: Public domain W3C validator