Theorem nfralxy 2402

Description: Not-free for restricted universal quantification where x and y are distinct. See nfralya 2404 for a version with y and A distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

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 1395	. . 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 2398	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	trud 1293	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1285   F/wnf 1389   F/_wnfc 2206   A.wral 2348

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1376  ax-7 1377  ax-gen 1378  ax-ie1 1422  ax-ie2 1423  ax-4 1440  ax-17 1459  ax-ial 1467  ax-i5r 1468  ax-ext 2063

This theorem depends on definitions:  df-bi 115  df-tru 1287  df-nf 1390  df-cleq 2074  df-clel 2077  df-nfc 2208  df-ral 2353

This theorem is referenced by:  nfra2xy  2406  rspc2  2711  sbcralt  2890  sbcralg  2892  raaanlem  3346  nfint  3646  nfiinxy  3705  nfpo  4056  nfso  4057  nfse  4096  nffrfor  4103  nfwe  4110  ralxpf  4500  funimaexglem  5002  fun11iun  5167  dff13f  5430  nfiso  5466  mpt2eq123  5584  fmpt2x  5846  nfrecs  5945  ac6sfi  6379  lble  8025  fzrevral  9122  bezoutlemmain  10387  setindis  10762  bdsetindis  10764