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  3936  nfiinxy  3995  nfpo  4396  nfso  4397  nfse  4436  nffrfor  4443  nfwe  4450  ralxpf  4874  funimaexglem  5410  fun11iun  5601  dff13f  5906  nfiso  5942  mpoeq123  6075  nfofr  6237  fmpox  6360  nfrecs  6468  xpf1o  7025  ac6sfi  7080  ismkvnex  7345  lble  9117  fzrevral  10330  nfsum1  11907  nfsum  11908  fsum2dlemstep  11985  fisumcom2  11989  nfcprod1  12105  nfcprod  12106  bezoutlemmain  12559  cnmpt21  15005  setindis  16498  bdsetindis  16500  strcollnfALT  16517  isomninnlem  16570  iswomninnlem  16589  ismkvnnlem  16592