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

Theorem nfralxy 2357
Description: Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfralya 2359 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 1355 . . 3 𝑦
2 nfralxy.1 . . . 4 𝑥𝐴
32a1i 9 . . 3 (⊤ → 𝑥𝐴)
4 nfralxy.2 . . . 4 𝑥𝜑
54a1i 9 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfraldxy 2353 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1252 1 𝑥𝑦𝐴 𝜑
Colors of variables: wff set class
Syntax hints:  wtru 1244  wnf 1349  wnfc 2165  wral 2303
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-4 1400  ax-17 1419  ax-ial 1427  ax-i5r 1428  ax-ext 2022
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308
This theorem is referenced by:  nfra2xy  2361  rspc2  2658  sbcralt  2831  sbcralg  2833  raaanlem  3323  nfint  3622  nfiinxy  3681  nfpo  4035  nfso  4036  nfse  4069  ralxpf  4445  funimaexglem  4945  fun11iun  5110  dff13f  5372  nfiso  5409  mpt2eq123  5527  fmpt2x  5789  nfrecs  5885  ac6sfi  6314  fzrevral  8910  setindis  9941  bdsetindis  9943
  Copyright terms: Public domain W3C validator