Theorem nfralxy 2408

Description: Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfralya 2410 for a version with 𝑦 and 𝐴 distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)

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 1396	. . 3 ⊢ Ⅎ𝑦⊤
2		nfralxy.1	. . . 4 ⊢ Ⅎ𝑥𝐴
3	2	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝐴)
4		nfralxy.2	. . . 4 ⊢ Ⅎ𝑥𝜑
5	4	a1i 9	. . 3 ⊢ (⊤ → Ⅎ𝑥𝜑)
6	1, 3, 5	nfraldxy 2404	. 2 ⊢ (⊤ → Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑)
7	6	trud 1294	1 ⊢ Ⅎ𝑥∀𝑦 ∈ 𝐴 𝜑

Syntax hints:  ⊤wtru 1286  Ⅎwnf 1390  Ⅎwnfc 2210  ∀wral 2353

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-4 1441  ax-17 1460  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-tru 1288  df-nf 1391  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358

This theorem is referenced by:  nfra2xy  2412  rspc2  2721  sbcralt  2901  sbcralg  2903  raaanlem  3368  nfint  3672  nfiinxy  3731  nfpo  4092  nfso  4093  nfse  4132  nffrfor  4139  nfwe  4146  ralxpf  4540  funimaexglem  5050  fun11iun  5222  dff13f  5489  nfiso  5525  mpt2eq123  5643  nfofr  5797  fmpt2x  5905  nfrecs  6004  xpf1o  6490  ac6sfi  6544  lble  8302  fzrevral  9412  nfsum1  10567  nfsum  10568  bezoutlemmain  10767  setindis  11205  bdsetindis  11207