Theorem nfra1 2563

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 2515	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1589	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1522	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1395   F/wnf 1508   e. wcel 2202   A.wral 2510

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 1495  ax-gen 1497  ax-ial 1582

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-ral 2515

This theorem is referenced by:  nfra2xy  2574  r19.12  2639  ralbi  2665  rexbi  2666  nfss  3220  ralidm  3595  nfii1  4001  dfiun2g  4002  mpteq12f  4169  reusv1  4555  ralxfrALT  4564  peano2  4693  fun11iun  5604  fvmptssdm  5731  ffnfv  5805  riota5f  5997  mpoeq123  6079  tfri3  6532  nfixp1  6886  nneneq  7042  exmidomni  7340  mkvprop  7356  caucvgsrlemgt1  8014  suplocsrlem  8027  lble  9126  indstr  9826  zsupcllemstep  10488  nninfinf  10704  fimaxre2  11787  prodeq2  12117  bezoutlemmain  12568  bezoutlemzz  12572  exmidunben  13046  mulcncf  15331  limccnp2cntop  15400  bj-rspgt  16382  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656