Theorem nfra1 2528

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

Syntax hints:   → wi 4  ∀wal 1362  Ⅎwnf 1474   ∈ wcel 2167  ∀wral 2475

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 1461  ax-gen 1463  ax-ial 1548

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-ral 2480

This theorem is referenced by:  nfra2xy  2539  r19.12  2603  ralbi  2629  rexbi  2630  nfss  3177  ralidm  3552  nfii1  3948  dfiun2g  3949  mpteq12f  4114  reusv1  4494  ralxfrALT  4503  peano2  4632  fun11iun  5528  fvmptssdm  5649  ffnfv  5723  riota5f  5905  mpoeq123  5985  tfri3  6434  nfixp1  6786  nneneq  6927  exmidomni  7217  mkvprop  7233  caucvgsrlemgt1  7881  suplocsrlem  7894  lble  8993  indstr  9686  zsupcllemstep  10338  nninfinf  10554  fimaxre2  11411  prodeq2  11741  bezoutlemmain  12192  bezoutlemzz  12196  exmidunben  12670  mulcncf  14952  limccnp2cntop  15021  bj-rspgt  15540  isomninnlem  15787  iswomninnlem  15806  ismkvnnlem  15809