Theorem nfralxy 2582

Description: Old name for nfralw 2581. (Contributed by Jim Kingdon, 30-May-2018.) (New usage is discouraged.)

Hypotheses

Ref	Expression
nfralxy.1	|- F/_ x A
nfralxy.2	|- F/ x ph

Assertion

Ref	Expression
nfralxy	|- F/ x A. y e. A ph

Distinct variable group:   x, y

Allowed substitution hints:   ph( x, y)   A( x, y)

Proof of Theorem nfralxy

Step	Hyp	Ref	Expression
1		nftru 1515	. . 3 |- F/ y T.
2		nfralxy.1	. . . 4 |- F/_ x A
3	2	a1i 9	. . 3 |- ( T. -> F/_ x A )
4		nfralxy.2	. . . 4 |- F/ x ph
5	4	a1i 9	. . 3 |- ( T. -> F/ x ph )
6	1, 3, 5	nfraldxy 2577	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1407	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1399   F/wnf 1509   F/_wnfc 2373   A.wral 2522

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-4 1559  ax-17 1575  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527

This theorem is referenced by:  nfra2xy  2586  rspc2  2935  sbcralt  3122  sbcralg  3124  raaanlem  3618  nfint  3964  nfiinxy  4023  nfpo  4427  nfso  4428  nfse  4467  nffrfor  4474  nfwe  4481  ralxpf  4906  funimaexglem  5444  fun11iun  5640  dff13f  5949  nfiso  5985  mpoeq123  6120  nfofr  6282  fmpox  6409  nfrecs  6551  xpf1o  7110  ac6sfi  7168  ismkvnex  7459  lble  9238  fzrevral  10461  nfsum1  12066  nfsum  12067  fsum2dlemstep  12145  fisumcom2  12149  nfcprod1  12265  nfcprod  12266  bezoutlemmain  12719  cnmpt21  15282  setindis  16863  bdsetindis  16865  strcollnfALT  16882  isomninnlem  16940  iswomninnlem  16960  ismkvnnlem  16963