Theorem nfra1 2581

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

This proof depends on syntax axioms:   → wi 4  ∀wal 1400  Ⅎwnf 1513   ∈ wcel 2209  ∀wral 2528

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-ial 1587

This proof depends on definitions:  df-bi 117  df-nf 1514  df-ral 2533

This theorem is used by:  nfra2xy  2592  r19.12  2657  ralbi  2683  rexbi  2684  nfss  3241  ralidm  3628  nfii1  4043  dfiun2g  4044  mpteq12f  4212  reusv1  4606  ralxfrALT  4615  peano2  4744  fun11iun  5663  fvmptssdm  5793  ffnfv  5869  riota5f  6068  mpoeq123  6150  abrexss  6362  tfri3  6643  nfixp1  7006  nneneq  7164  exmidomni  7488  mkvprop  7504  caucvgsrlemgt1  8168  suplocsrlem  8181  lble  9285  indstr  10008  zsupcllemstep  10678  nninfinf  10900  fimaxre2  12015  prodeq2  12348  bezoutlemmain  12799  bezoutlemzz  12803  exmidunben  13374  mulcncf  15851  limccnp2cntop  15920  bj-rspgt  17036  isomninnlem  17302  iswomninnlem  17323  ismkvnnlem  17326