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

Theorem nfra1 2352
 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 2308 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1434 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1363 1 𝑥𝑥𝐴 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1241  Ⅎwnf 1349   ∈ wcel 1393  ∀wral 2303 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 1336  ax-gen 1338  ax-ial 1427 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-ral 2308 This theorem is referenced by:  nfra2xy  2361  r19.12  2419  ralbi  2442  rexbi  2443  nfss  2935  ralidm  3318  nfii1  3685  dfiun2g  3686  mpteq12f  3834  reusv1  4162  ralxfrALT  4171  peano2  4281  fun11iun  5110  fvmptssdm  5218  ffnfv  5286  riota5f  5455  mpt2eq123  5527  tfri3  5916  nneneq  6283  caucvgsrlemgt1  6836  indstr  8484  bj-rspgt  9774
 Copyright terms: Public domain W3C validator