Theorem nfralxy 2508

Description: Old name for nfralw 2507. (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 1459	. . 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 2503	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1357	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1349   F/wnf 1453   F/_wnfc 2299   A.wral 2448

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-4 1503  ax-17 1519  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-tru 1351  df-nf 1454  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453

This theorem is referenced by:  nfra2xy  2512  rspc2  2845  sbcralt  3031  sbcralg  3033  raaanlem  3520  nfint  3841  nfiinxy  3900  nfpo  4286  nfso  4287  nfse  4326  nffrfor  4333  nfwe  4340  ralxpf  4757  funimaexglem  5281  fun11iun  5463  dff13f  5749  nfiso  5785  mpoeq123  5912  nfofr  6067  fmpox  6179  nfrecs  6286  xpf1o  6822  ac6sfi  6876  ismkvnex  7131  lble  8863  fzrevral  10061  nfsum1  11319  nfsum  11320  fsum2dlemstep  11397  fisumcom2  11401  nfcprod1  11517  nfcprod  11518  bezoutlemmain  11953  cnmpt21  13085  setindis  14002  bdsetindis  14004  strcollnfALT  14021  isomninnlem  14062  iswomninnlem  14081  ismkvnnlem  14084