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  2854  sbcralt  3041  sbcralg  3043  raaanlem  3530  nfint  3856  nfiinxy  3915  nfpo  4303  nfso  4304  nfse  4343  nffrfor  4350  nfwe  4357  ralxpf  4775  funimaexglem  5301  fun11iun  5484  dff13f  5773  nfiso  5809  mpoeq123  5936  nfofr  6091  fmpox  6203  nfrecs  6310  xpf1o  6846  ac6sfi  6900  ismkvnex  7155  lble  8906  fzrevral  10107  nfsum1  11366  nfsum  11367  fsum2dlemstep  11444  fisumcom2  11448  nfcprod1  11564  nfcprod  11565  bezoutlemmain  12001  cnmpt21  13876  setindis  14804  bdsetindis  14806  strcollnfALT  14823  isomninnlem  14863  iswomninnlem  14882  ismkvnnlem  14885