Theorem nfra1 2539

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 2491	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))
2		nfa1 1565	. 2 ⊢ Ⅎ𝑥∀𝑥(𝑥 ∈ 𝐴 → 𝜑)
3	1, 2	nfxfr 1498	1 ⊢ Ⅎ𝑥∀𝑥 ∈ 𝐴 𝜑

Syntax hints:   → wi 4  ∀wal 1371  Ⅎwnf 1484   ∈ wcel 2178  ∀wral 2486

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-ial 1558

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-ral 2491

This theorem is referenced by:  nfra2xy  2550  r19.12  2614  ralbi  2640  rexbi  2641  nfss  3194  ralidm  3569  nfii1  3972  dfiun2g  3973  mpteq12f  4140  reusv1  4523  ralxfrALT  4532  peano2  4661  fun11iun  5565  fvmptssdm  5687  ffnfv  5761  riota5f  5947  mpoeq123  6027  tfri3  6476  nfixp1  6828  nneneq  6979  exmidomni  7270  mkvprop  7286  caucvgsrlemgt1  7943  suplocsrlem  7956  lble  9055  indstr  9749  zsupcllemstep  10409  nninfinf  10625  fimaxre2  11653  prodeq2  11983  bezoutlemmain  12434  bezoutlemzz  12438  exmidunben  12912  mulcncf  15195  limccnp2cntop  15264  bj-rspgt  15922  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193