Theorem nfralxy 2535

Description: Old name for nfralw 2534. (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 1480	. . 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 2530	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1373	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1365   F/wnf 1474   F/_wnfc 2326   A.wral 2475

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-4 1524  ax-17 1540  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480

This theorem is referenced by:  nfra2xy  2539  rspc2  2879  sbcralt  3066  sbcralg  3068  raaanlem  3555  nfint  3884  nfiinxy  3943  nfpo  4336  nfso  4337  nfse  4376  nffrfor  4383  nfwe  4390  ralxpf  4812  funimaexglem  5341  fun11iun  5525  dff13f  5817  nfiso  5853  mpoeq123  5981  nfofr  6142  fmpox  6258  nfrecs  6365  xpf1o  6905  ac6sfi  6959  ismkvnex  7221  lble  8974  fzrevral  10180  nfsum1  11521  nfsum  11522  fsum2dlemstep  11599  fisumcom2  11603  nfcprod1  11719  nfcprod  11720  bezoutlemmain  12165  cnmpt21  14527  setindis  15613  bdsetindis  15615  strcollnfALT  15632  isomninnlem  15674  iswomninnlem  15693  ismkvnnlem  15696