Theorem nfralxy 2568

Description: Old name for nfralw 2567. (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 1512	. . 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 2563	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1404	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1396   F/wnf 1506   F/_wnfc 2359   A.wral 2508

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  nfra2xy  2572  rspc2  2919  sbcralt  3106  sbcralg  3108  raaanlem  3597  nfint  3934  nfiinxy  3993  nfpo  4394  nfso  4395  nfse  4434  nffrfor  4441  nfwe  4448  ralxpf  4872  funimaexglem  5408  fun11iun  5599  dff13f  5904  nfiso  5940  mpoeq123  6073  nfofr  6235  fmpox  6358  nfrecs  6466  xpf1o  7023  ac6sfi  7078  ismkvnex  7343  lble  9115  fzrevral  10328  nfsum1  11904  nfsum  11905  fsum2dlemstep  11982  fisumcom2  11986  nfcprod1  12102  nfcprod  12103  bezoutlemmain  12556  cnmpt21  15002  setindis  16472  bdsetindis  16474  strcollnfALT  16491  isomninnlem  16544  iswomninnlem  16563  ismkvnnlem  16566