Theorem nfra1 2466

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 2421	. 2 |- ( A. x e. A ph <-> A. x ( x e. A -> ph ) )
2		nfa1 1521	. 2 |- F/ x A. x ( x e. A -> ph )
3	1, 2	nfxfr 1450	1 |- F/ x A. x e. A ph

Syntax hints:   -> wi 4   A.wal 1329   F/wnf 1436   e. wcel 1480   A.wral 2416

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 1423  ax-gen 1425  ax-ial 1514

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-ral 2421

This theorem is referenced by:  nfra2xy  2475  r19.12  2538  ralbi  2564  rexbi  2565  nfss  3090  ralidm  3463  nfii1  3844  dfiun2g  3845  mpteq12f  4008  reusv1  4379  ralxfrALT  4388  peano2  4509  fun11iun  5388  fvmptssdm  5505  ffnfv  5578  riota5f  5754  mpoeq123  5830  tfri3  6264  nfixp1  6612  nneneq  6751  exmidomni  7014  mkvprop  7032  caucvgsrlemgt1  7603  suplocsrlem  7616  lble  8705  indstr  9388  fimaxre2  10998  prodeq2  11326  zsupcllemstep  11638  bezoutlemmain  11686  bezoutlemzz  11690  exmidunben  11939  mulcncf  12760  limccnp2cntop  12815  bj-rspgt  12993  isomninnlem  13225