Theorem nfra1 2561

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 2513	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1587	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1520	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1393   F/wnf 1506   e. wcel 2200   A.wral 2508

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 1493  ax-gen 1495  ax-ial 1580

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-ral 2513

This theorem is referenced by:  nfra2xy  2572  r19.12  2637  ralbi  2663  rexbi  2664  nfss  3217  ralidm  3592  nfii1  3996  dfiun2g  3997  mpteq12f  4164  reusv1  4549  ralxfrALT  4558  peano2  4687  fun11iun  5595  fvmptssdm  5721  ffnfv  5795  riota5f  5987  mpoeq123  6069  tfri3  6519  nfixp1  6873  nneneq  7026  exmidomni  7320  mkvprop  7336  caucvgsrlemgt1  7993  suplocsrlem  8006  lble  9105  indstr  9800  zsupcllemstep  10461  nninfinf  10677  fimaxre2  11754  prodeq2  12084  bezoutlemmain  12535  bezoutlemzz  12539  exmidunben  13013  mulcncf  15298  limccnp2cntop  15367  bj-rspgt  16233  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508