Theorem nfralxy 2568

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

Syntax hints:  ⊤wtru 1396  Ⅎwnf 1506  Ⅎwnfc 2359  ∀wral 2508

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-4 1556  ax-17 1572  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513

This theorem is referenced by:  nfra2xy  2572  rspc2  2918  sbcralt  3105  sbcralg  3107  raaanlem  3596  nfint  3933  nfiinxy  3992  nfpo  4392  nfso  4393  nfse  4432  nffrfor  4439  nfwe  4446  ralxpf  4868  funimaexglem  5404  fun11iun  5595  dff13f  5900  nfiso  5936  mpoeq123  6069  nfofr  6231  fmpox  6352  nfrecs  6459  xpf1o  7013  ac6sfi  7068  ismkvnex  7333  lble  9105  fzrevral  10313  nfsum1  11883  nfsum  11884  fsum2dlemstep  11961  fisumcom2  11965  nfcprod1  12081  nfcprod  12082  bezoutlemmain  12535  cnmpt21  14981  setindis  16413  bdsetindis  16415  strcollnfALT  16432  isomninnlem  16486  iswomninnlem  16505  ismkvnnlem  16508