Theorem nfra1 2497

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 2449	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1529	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1462	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1341   F/wnf 1448   e. wcel 2136   A.wral 2444

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-gen 1437  ax-ial 1522

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-ral 2449

This theorem is referenced by:  nfra2xy  2508  r19.12  2572  ralbi  2598  rexbi  2599  nfss  3135  ralidm  3509  nfii1  3897  dfiun2g  3898  mpteq12f  4062  reusv1  4436  ralxfrALT  4445  peano2  4572  fun11iun  5453  fvmptssdm  5570  ffnfv  5643  riota5f  5822  mpoeq123  5901  tfri3  6335  nfixp1  6684  nneneq  6823  exmidomni  7106  mkvprop  7122  caucvgsrlemgt1  7736  suplocsrlem  7749  lble  8842  indstr  9531  fimaxre2  11168  prodeq2  11498  zsupcllemstep  11878  bezoutlemmain  11931  bezoutlemzz  11935  exmidunben  12359  mulcncf  13231  limccnp2cntop  13286  bj-rspgt  13667  isomninnlem  13909  iswomninnlem  13928  ismkvnnlem  13931