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  3218  ralidm  3593  nfii1  3999  dfiun2g  4000  mpteq12f  4167  reusv1  4553  ralxfrALT  4562  peano2  4691  fun11iun  5601  fvmptssdm  5727  ffnfv  5801  riota5f  5993  mpoeq123  6075  tfri3  6528  nfixp1  6882  nneneq  7038  exmidomni  7332  mkvprop  7348  caucvgsrlemgt1  8005  suplocsrlem  8018  lble  9117  indstr  9817  zsupcllemstep  10479  nninfinf  10695  fimaxre2  11778  prodeq2  12108  bezoutlemmain  12559  bezoutlemzz  12563  exmidunben  13037  mulcncf  15322  limccnp2cntop  15391  bj-rspgt  16318  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592