Theorem nfralxy 2513

Description: Old name for nfralw 2512. (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 1464	. . 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 2508	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1362	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1354   F/wnf 1458   F/_wnfc 2304   A.wral 2453

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-4 1508  ax-17 1524  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458

This theorem is referenced by:  nfra2xy  2517  rspc2  2850  sbcralt  3037  sbcralg  3039  raaanlem  3526  nfint  3850  nfiinxy  3909  nfpo  4295  nfso  4296  nfse  4335  nffrfor  4342  nfwe  4349  ralxpf  4766  funimaexglem  5291  fun11iun  5474  dff13f  5761  nfiso  5797  mpoeq123  5924  nfofr  6079  fmpox  6191  nfrecs  6298  xpf1o  6834  ac6sfi  6888  ismkvnex  7143  lble  8875  fzrevral  10073  nfsum1  11330  nfsum  11331  fsum2dlemstep  11408  fisumcom2  11412  nfcprod1  11528  nfcprod  11529  bezoutlemmain  11964  cnmpt21  13342  setindis  14259  bdsetindis  14261  strcollnfALT  14278  isomninnlem  14319  iswomninnlem  14338  ismkvnnlem  14341