Theorem nfra1 2501

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

Step	Hyp	Ref	Expression
1		df-ral 2453	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 1534	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1467	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1346  Ⅎwnf 1453   ∈ wcel 2141  ∀wral 2448

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 1440  ax-gen 1442  ax-ial 1527

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-ral 2453

This theorem is referenced by:  nfra2xy  2512  r19.12  2576  ralbi  2602  rexbi  2603  nfss  3140  ralidm  3514  nfii1  3902  dfiun2g  3903  mpteq12f  4067  reusv1  4441  ralxfrALT  4450  peano2  4577  fun11iun  5461  fvmptssdm  5578  ffnfv  5651  riota5f  5830  mpoeq123  5909  tfri3  6343  nfixp1  6692  nneneq  6831  exmidomni  7114  mkvprop  7130  caucvgsrlemgt1  7744  suplocsrlem  7757  lble  8850  indstr  9539  fimaxre2  11177  prodeq2  11507  zsupcllemstep  11887  bezoutlemmain  11940  bezoutlemzz  11944  exmidunben  12368  mulcncf  13344  limccnp2cntop  13399  bj-rspgt  13780  isomninnlem  14022  iswomninnlem  14041  ismkvnnlem  14044