Theorem nfralxy 2570

Description: Old name for nfralw 2569. (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 1514	. . 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 2565	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1406	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1398   F/wnf 1508   F/_wnfc 2361   A.wral 2510

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  nfra2xy  2574  rspc2  2921  sbcralt  3108  sbcralg  3110  raaanlem  3599  nfint  3938  nfiinxy  3997  nfpo  4398  nfso  4399  nfse  4438  nffrfor  4445  nfwe  4452  ralxpf  4876  funimaexglem  5413  fun11iun  5604  dff13f  5910  nfiso  5946  mpoeq123  6079  nfofr  6241  fmpox  6364  nfrecs  6472  xpf1o  7029  ac6sfi  7086  ismkvnex  7353  lble  9126  fzrevral  10339  nfsum1  11916  nfsum  11917  fsum2dlemstep  11994  fisumcom2  11998  nfcprod1  12114  nfcprod  12115  bezoutlemmain  12568  cnmpt21  15014  setindis  16562  bdsetindis  16564  strcollnfALT  16581  isomninnlem  16634  iswomninnlem  16653  ismkvnnlem  16656