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  4211  reusv1  4604  ralxfrALT  4613  peano2  4742  fun11iun  5660  fvmptssdm  5790  ffnfv  5866  riota5f  6065  mpoeq123  6147  abrexss  6358  tfri3  6638  nfixp1  7000  nneneq  7158  exmidomni  7482  mkvprop  7498  caucvgsrlemgt1  8162  suplocsrlem  8175  lble  9277  indstr  9993  zsupcllemstep  10662  nninfinf  10880  fimaxre2  11993  prodeq2  12324  bezoutlemmain  12775  bezoutlemzz  12779  exmidunben  13317  mulcncf  15709  limccnp2cntop  15778  bj-rspgt  16814  isomninnlem  17079  iswomninnlem  17099  ismkvnnlem  17102