Theorem nfra1 2563

Description: x is not free in A. x e. A ph. (Contributed by NM, 18-Oct-1996.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfra1	|- F/ x A. x e. A ph

Proof of Theorem nfra1

Step	Hyp	Ref	Expression
1		df-ral 2515	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1589	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1522	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1395   F/wnf 1508   e. wcel 2202   A.wral 2510

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 1495  ax-gen 1497  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  nfra2xy  2574  r19.12  2639  ralbi  2665  rexbi  2666  nfss  3220  ralidm  3595  nfii1  4001  dfiun2g  4002  mpteq12f  4169  reusv1  4555  ralxfrALT  4564  peano2  4693  fun11iun  5604  fvmptssdm  5731  ffnfv  5805  riota5f  5998  mpoeq123  6080  tfri3  6533  nfixp1  6887  nneneq  7043  exmidomni  7341  mkvprop  7357  caucvgsrlemgt1  8015  suplocsrlem  8028  lble  9127  indstr  9827  zsupcllemstep  10490  nninfinf  10706  fimaxre2  11805  prodeq2  12136  bezoutlemmain  12587  bezoutlemzz  12591  exmidunben  13065  mulcncf  15351  limccnp2cntop  15420  bj-rspgt  16433  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708