Theorem nfralxy 2515

Description: Old name for nfralw 2514. (Contributed by Jim Kingdon, 30-May-2018.) (New usage is discouraged.)

Hypotheses

Ref	Expression
nfralxy.1	⊢ Ⅎ𝑥𝐴
nfralxy.2	⊢ Ⅎ𝑥𝜑

Assertion

Ref	Expression
nfralxy	⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Distinct variable group:   𝑥,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑦)   𝐴(𝑥,𝑦)

Proof of Theorem nfralxy

Step	Hyp	Ref	Expression
1		nftru 1466	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralxy.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralxy.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldxy 2510	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1362	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1354  Ⅎwnf 1460  Ⅎwnfc 2306  ∀wral 2455

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-4 1510  ax-17 1526  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460

This theorem is referenced by:  nfra2xy  2519  rspc2  2852  sbcralt  3039  sbcralg  3041  raaanlem  3528  nfint  3854  nfiinxy  3913  nfpo  4301  nfso  4302  nfse  4341  nffrfor  4348  nfwe  4355  ralxpf  4773  funimaexglem  5299  fun11iun  5482  dff13f  5770  nfiso  5806  mpoeq123  5933  nfofr  6088  fmpox  6200  nfrecs  6307  xpf1o  6843  ac6sfi  6897  ismkvnex  7152  lble  8903  fzrevral  10104  nfsum1  11363  nfsum  11364  fsum2dlemstep  11441  fisumcom2  11445  nfcprod1  11561  nfcprod  11562  bezoutlemmain  11998  cnmpt21  13761  setindis  14689  bdsetindis  14691  strcollnfALT  14708  isomninnlem  14748  iswomninnlem  14767  ismkvnnlem  14770