Theorem nfra1 2488

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 2440	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1521	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1454	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1333   F/wnf 1440   e. wcel 2128   A.wral 2435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1427  ax-gen 1429  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1441  df-ral 2440

This theorem is referenced by:  nfra2xy  2499  r19.12  2563  ralbi  2589  rexbi  2590  nfss  3121  ralidm  3494  nfii1  3880  dfiun2g  3881  mpteq12f  4044  reusv1  4416  ralxfrALT  4425  peano2  4552  fun11iun  5432  fvmptssdm  5549  ffnfv  5622  riota5f  5798  mpoeq123  5874  tfri3  6308  nfixp1  6656  nneneq  6795  exmidomni  7068  mkvprop  7084  caucvgsrlemgt1  7698  suplocsrlem  7711  lble  8801  indstr  9487  fimaxre2  11108  prodeq2  11436  zsupcllemstep  11813  bezoutlemmain  11862  bezoutlemzz  11866  exmidunben  12127  mulcncf  12951  limccnp2cntop  13006  bj-rspgt  13319  isomninnlem  13563  iswomninnlem  13582  ismkvnnlem  13585