Theorem nfra1 2420

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

Syntax hints:   → wi 4  ∀wal 1294  Ⅎwnf 1401   ∈ wcel 1445  ∀wral 2370

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1388  ax-gen 1390  ax-ial 1479

This theorem depends on definitions:  df-bi 116  df-nf 1402  df-ral 2375

This theorem is referenced by:  nfra2xy  2429  r19.12  2491  ralbi  2515  rexbi  2516  nfss  3032  ralidm  3402  nfii1  3783  dfiun2g  3784  mpteq12f  3940  reusv1  4308  ralxfrALT  4317  peano2  4438  fun11iun  5309  fvmptssdm  5423  ffnfv  5495  riota5f  5670  mpt2eq123  5746  tfri3  6170  nfixp1  6515  nneneq  6653  exmidomni  6885  mkvprop  6901  caucvgsrlemgt1  7437  lble  8505  indstr  9180  fimaxre2  10773  zsupcllemstep  11368  bezoutlemmain  11414  bezoutlemzz  11418  mulcncf  12354  bj-rspgt  12394