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  2918  sbcralt  3105  sbcralg  3107  raaanlem  3596  nfint  3933  nfiinxy  3992  nfpo  4392  nfso  4393  nfse  4432  nffrfor  4439  nfwe  4446  ralxpf  4868  funimaexglem  5404  fun11iun  5593  dff13f  5894  nfiso  5930  mpoeq123  6063  nfofr  6225  fmpox  6346  nfrecs  6453  xpf1o  7005  ac6sfi  7060  ismkvnex  7322  lble  9094  fzrevral  10301  nfsum1  11867  nfsum  11868  fsum2dlemstep  11945  fisumcom2  11949  nfcprod1  12065  nfcprod  12066  bezoutlemmain  12519  cnmpt21  14965  setindis  16330  bdsetindis  16332  strcollnfALT  16349  isomninnlem  16398  iswomninnlem  16417  ismkvnnlem  16420