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

Theorem nfralxy 2354
Description: Not-free for restricted universal quantification where and are distinct. See nfralya 2356 for a version with and distinct instead. (Contributed by Jim Kingdon, 30-May-2018.)
Hypotheses
Ref Expression
nfralxy.1  F/_
nfralxy.2  F/
Assertion
Ref Expression
nfralxy  F/
Distinct variable group:   ,
Allowed substitution hints:   (,)   (,)

Proof of Theorem nfralxy
StepHypRef Expression
1 nftru 1352 . . 3  F/
2 nfralxy.1 . . . 4  F/_
32a1i 9 . . 3  F/_
4 nfralxy.2 . . . 4  F/
54a1i 9 . . 3  F/
61, 3, 5nfraldxy 2350 . 2  F/
76trud 1251 1  F/
Colors of variables: wff set class
Syntax hints:   wtru 1243   F/wnf 1346   F/_wnfc 2162  wral 2300
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 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-4 1397  ax-17 1416  ax-ial 1424  ax-i5r 1425  ax-ext 2019
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305
This theorem is referenced by:  nfra2xy  2358  rspc2  2655  sbcralt  2828  sbcralg  2830  raaanlem  3320  nfint  3616  nfiinxy  3675  nfpo  4029  nfso  4030  nfse  4063  ralxpf  4425  funimaexglem  4925  fun11iun  5090  dff13f  5352  nfiso  5389  mpt2eq123  5506  fmpt2x  5768  nfrecs  5863  fzrevral  8697  setindis  9351  bdsetindis  9353
  Copyright terms: Public domain W3C validator