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

Theorem nfralxy 2377
 Description: Not-free for restricted universal quantification where 𝑥 and 𝑦 are distinct. See nfralya 2379 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 1371 . . 3 𝑦
2 nfralxy.1 . . . 4 𝑥𝐴
32a1i 9 . . 3 (⊤ → 𝑥𝐴)
4 nfralxy.2 . . . 4 𝑥𝜑
54a1i 9 . . 3 (⊤ → Ⅎ𝑥𝜑)
61, 3, 5nfraldxy 2373 . 2 (⊤ → Ⅎ𝑥𝑦𝐴 𝜑)
76trud 1268 1 𝑥𝑦𝐴 𝜑
 Colors of variables: wff set class Syntax hints:  ⊤wtru 1260  Ⅎwnf 1365  Ⅎwnfc 2181  ∀wral 2323 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-4 1416  ax-17 1435  ax-ial 1443  ax-i5r 1444  ax-ext 2038 This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-cleq 2049  df-clel 2052  df-nfc 2183  df-ral 2328 This theorem is referenced by:  nfra2xy  2381  rspc2  2683  sbcralt  2862  sbcralg  2864  raaanlem  3354  nfint  3653  nfiinxy  3712  nfpo  4066  nfso  4067  nfse  4106  nffrfor  4113  nfwe  4120  ralxpf  4510  funimaexglem  5010  fun11iun  5175  dff13f  5437  nfiso  5474  mpt2eq123  5592  fmpt2x  5854  nfrecs  5953  ac6sfi  6383  fzrevral  9069  setindis  10479  bdsetindis  10481
 Copyright terms: Public domain W3C validator