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  5593  fvmptssdm  5719  ffnfv  5793  riota5f  5981  mpoeq123  6063  tfri3  6513  nfixp1  6865  nneneq  7018  exmidomni  7309  mkvprop  7325  caucvgsrlemgt1  7982  suplocsrlem  7995  lble  9094  indstr  9788  zsupcllemstep  10449  nninfinf  10665  fimaxre2  11738  prodeq2  12068  bezoutlemmain  12519  bezoutlemzz  12523  exmidunben  12997  mulcncf  15282  limccnp2cntop  15351  bj-rspgt  16150  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420