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

Theorem nfra1 2466
 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 2421 . 2 (∀𝑥𝐴 𝜑 ↔ ∀𝑥(𝑥𝐴𝜑))
2 nfa1 1521 . 2 𝑥𝑥(𝑥𝐴𝜑)
31, 2nfxfr 1450 1 𝑥𝑥𝐴 𝜑
 Colors of variables: wff set class Syntax hints:   → wi 4  ∀wal 1329  Ⅎwnf 1436   ∈ wcel 1480  ∀wral 2416 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-gen 1425  ax-ial 1514 This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421 This theorem is referenced by:  nfra2xy  2475  r19.12  2538  ralbi  2564  rexbi  2565  nfss  3090  ralidm  3463  nfii1  3844  dfiun2g  3845  mpteq12f  4008  reusv1  4379  ralxfrALT  4388  peano2  4509  fun11iun  5388  fvmptssdm  5505  ffnfv  5578  riota5f  5754  mpoeq123  5830  tfri3  6264  nfixp1  6612  nneneq  6751  exmidomni  7014  mkvprop  7032  caucvgsrlemgt1  7610  suplocsrlem  7623  lble  8712  indstr  9395  fimaxre2  11005  prodeq2  11333  zsupcllemstep  11645  bezoutlemmain  11693  bezoutlemzz  11697  exmidunben  11946  mulcncf  12770  limccnp2cntop  12825  bj-rspgt  13023  isomninnlem  13255
 Copyright terms: Public domain W3C validator