ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  nfralxy GIF version

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
StepHypRef Expression
1 nftru 1396 . . 3 𝑦
2 nfralxy.1 . . . 4 𝑥𝐴
32a1i 9 . . 3 (⊤ → 𝑥𝐴)
4 nfralxy.2 . . . 4 𝑥𝜑
54a1i 9 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfraldxy 2404 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1294 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff set class
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
  Copyright terms: Public domain W3C validator