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

Theorem nfralxy 2360
 Description: Not-free for restricted universal quantification where and are distinct. See nfralya 2362 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 2356 . 2
76trud 1252 1
 Colors of variables: wff set class Syntax hints:   wtru 1244  wnf 1349  wnfc 2165  wral 2306 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 2311 This theorem is referenced by:  nfra2xy  2364  rspc2  2661  sbcralt  2834  sbcralg  2836  raaanlem  3326  nfint  3625  nfiinxy  3684  nfpo  4038  nfso  4039  nfse  4078  nffrfor  4085  nfwe  4092  ralxpf  4482  funimaexglem  4982  fun11iun  5147  dff13f  5409  nfiso  5446  mpt2eq123  5564  fmpt2x  5826  nfrecs  5922  ac6sfi  6352  fzrevral  8967  setindis  10092  bdsetindis  10094
 Copyright terms: Public domain W3C validator