Theorem nfralxy 2469

Description: Not-free for restricted universal quantification where x and y are distinct. See nfralya 2471 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 1442	. . 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 2465	. 2 |- ( T. -> F/ x A. y e. A ph )
7	6	mptru 1340	1 |- F/ x A. y e. A ph

Syntax hints:   T. wtru 1332   F/wnf 1436   F/_wnfc 2266   A.wral 2414

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-4 1487  ax-17 1506  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-tru 1334  df-nf 1437  df-cleq 2130  df-clel 2133  df-nfc 2268  df-ral 2419

This theorem is referenced by:  nfra2xy  2473  rspc2  2795  sbcralt  2980  sbcralg  2982  raaanlem  3463  nfint  3776  nfiinxy  3835  nfpo  4218  nfso  4219  nfse  4258  nffrfor  4265  nfwe  4272  ralxpf  4680  funimaexglem  5201  fun11iun  5381  dff13f  5664  nfiso  5700  mpoeq123  5823  nfofr  5981  fmpox  6091  nfrecs  6197  xpf1o  6731  ac6sfi  6785  ismkvnex  7022  lble  8698  fzrevral  9878  nfsum1  11118  nfsum  11119  fsum2dlemstep  11196  fisumcom2  11200  nfcprod1  11316  nfcprod  11317  bezoutlemmain  11675  cnmpt21  12449  setindis  13154  bdsetindis  13156  isomninnlem  13214