Theorem nfralxy 2502

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

Syntax hints:  ⊤wtru 1343  Ⅎwnf 1447  Ⅎwnfc 2293  ∀wral 2442

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 1434  ax-7 1435  ax-gen 1436  ax-ie1 1480  ax-ie2 1481  ax-4 1497  ax-17 1513  ax-ial 1521  ax-i5r 1522  ax-ext 2146

This theorem depends on definitions:  df-bi 116  df-tru 1345  df-nf 1448  df-cleq 2157  df-clel 2160  df-nfc 2295  df-ral 2447

This theorem is referenced by:  nfra2xy  2506  rspc2  2836  sbcralt  3022  sbcralg  3024  raaanlem  3509  nfint  3828  nfiinxy  3887  nfpo  4273  nfso  4274  nfse  4313  nffrfor  4320  nfwe  4327  ralxpf  4744  funimaexglem  5265  fun11iun  5447  dff13f  5732  nfiso  5768  mpoeq123  5892  nfofr  6050  fmpox  6160  nfrecs  6266  xpf1o  6801  ac6sfi  6855  ismkvnex  7110  lble  8833  fzrevral  10030  nfsum1  11283  nfsum  11284  fsum2dlemstep  11361  fisumcom2  11365  nfcprod1  11481  nfcprod  11482  bezoutlemmain  11916  cnmpt21  12832  setindis  13684  bdsetindis  13686  strcollnfALT  13703  isomninnlem  13743  iswomninnlem  13762  ismkvnnlem  13765