Theorem nfralxy 2570

Description: Old name for nfralw 2569. (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 1514	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralxy.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralxy.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldxy 2565	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	mptru 1406	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1398  Ⅎwnf 1508  Ⅎwnfc 2361  ∀wral 2510

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-4 1558  ax-17 1574  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515

This theorem is referenced by:  nfra2xy  2574  rspc2  2921  sbcralt  3108  sbcralg  3110  raaanlem  3599  nfint  3938  nfiinxy  3997  nfpo  4398  nfso  4399  nfse  4438  nffrfor  4445  nfwe  4452  ralxpf  4876  funimaexglem  5413  fun11iun  5604  dff13f  5911  nfiso  5947  mpoeq123  6080  nfofr  6242  fmpox  6365  nfrecs  6473  xpf1o  7030  ac6sfi  7087  ismkvnex  7354  lble  9127  fzrevral  10340  nfsum1  11934  nfsum  11935  fsum2dlemstep  12013  fisumcom2  12017  nfcprod1  12133  nfcprod  12134  bezoutlemmain  12587  cnmpt21  15034  setindis  16613  bdsetindis  16615  strcollnfALT  16632  isomninnlem  16685  iswomninnlem  16705  ismkvnnlem  16708