Theorem nfralxy 2546

Description: Old name for nfralw 2545. (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 1490	. . 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 2541	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1382	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1374   F/wnf 1484   F/_wnfc 2337   A.wral 2486

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-4 1534  ax-17 1550  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-tru 1376  df-nf 1485  df-cleq 2200  df-clel 2203  df-nfc 2339  df-ral 2491

This theorem is referenced by:  nfra2xy  2550  rspc2  2895  sbcralt  3082  sbcralg  3084  raaanlem  3573  nfint  3909  nfiinxy  3968  nfpo  4366  nfso  4367  nfse  4406  nffrfor  4413  nfwe  4420  ralxpf  4842  funimaexglem  5376  fun11iun  5565  dff13f  5862  nfiso  5898  mpoeq123  6027  nfofr  6188  fmpox  6309  nfrecs  6416  xpf1o  6966  ac6sfi  7021  ismkvnex  7283  lble  9055  fzrevral  10262  nfsum1  11782  nfsum  11783  fsum2dlemstep  11860  fisumcom2  11864  nfcprod1  11980  nfcprod  11981  bezoutlemmain  12434  cnmpt21  14878  setindis  16102  bdsetindis  16104  strcollnfALT  16121  isomninnlem  16171  iswomninnlem  16190  ismkvnnlem  16193