Theorem nfra1 2518

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 2470	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1551	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1484	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1361   F/wnf 1470   e. wcel 2158   A.wral 2465

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 1457  ax-gen 1459  ax-ial 1544

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-ral 2470

This theorem is referenced by:  nfra2xy  2529  r19.12  2593  ralbi  2619  rexbi  2620  nfss  3160  ralidm  3535  nfii1  3929  dfiun2g  3930  mpteq12f  4095  reusv1  4470  ralxfrALT  4479  peano2  4606  fun11iun  5494  fvmptssdm  5613  ffnfv  5687  riota5f  5868  mpoeq123  5947  tfri3  6382  nfixp1  6732  nneneq  6871  exmidomni  7154  mkvprop  7170  caucvgsrlemgt1  7808  suplocsrlem  7821  lble  8918  indstr  9607  fimaxre2  11249  prodeq2  11579  zsupcllemstep  11960  bezoutlemmain  12013  bezoutlemzz  12017  exmidunben  12441  mulcncf  14387  limccnp2cntop  14442  bj-rspgt  14834  isomninnlem  15075  iswomninnlem  15094  ismkvnnlem  15097