Theorem nfra1 2508

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 2460	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1541	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1474	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1351   F/wnf 1460   e. wcel 2148   A.wral 2455

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 1447  ax-gen 1449  ax-ial 1534

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-ral 2460

This theorem is referenced by:  nfra2xy  2519  r19.12  2583  ralbi  2609  rexbi  2610  nfss  3150  ralidm  3525  nfii1  3919  dfiun2g  3920  mpteq12f  4085  reusv1  4460  ralxfrALT  4469  peano2  4596  fun11iun  5484  fvmptssdm  5602  ffnfv  5676  riota5f  5857  mpoeq123  5936  tfri3  6370  nfixp1  6720  nneneq  6859  exmidomni  7142  mkvprop  7158  caucvgsrlemgt1  7796  suplocsrlem  7809  lble  8906  indstr  9595  fimaxre2  11237  prodeq2  11567  zsupcllemstep  11948  bezoutlemmain  12001  bezoutlemzz  12005  exmidunben  12429  mulcncf  14176  limccnp2cntop  14231  bj-rspgt  14623  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885