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

Theorem raleqbi1dv 2660
 Description: Equality deduction for restricted universal quantifier. (Contributed by NM, 16-Nov-1995.)
Hypothesis
Ref Expression
raleqd.1
Assertion
Ref Expression
raleqbi1dv
Distinct variable groups:   ,   ,
Allowed substitution hints:   ()   ()

Proof of Theorem raleqbi1dv
StepHypRef Expression
1 raleq 2652 . 2
2 raleqd.1 . . 3
32ralbidv 2457 . 2
41, 3bitrd 187 1
 Colors of variables: wff set class Syntax hints:   wi 4   wb 104   wceq 1335  wral 2435 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2139 This theorem depends on definitions:  df-bi 116  df-tru 1338  df-nf 1441  df-sb 1743  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ral 2440 This theorem is referenced by:  frforeq2  4305  weeq2  4317  peano5  4556  isoeq4  5751  exmidomni  7079  pitonn  7762  peano1nnnn  7766  peano2nnnn  7767  peano5nnnn  7806  peano5nni  8830  1nn  8838  peano2nn  8839  dfuzi  9268  istopg  12368  isbasisg  12413  basis2  12417  eltg2  12424  ispsmet  12694  ismet  12715  isxmet  12716  metrest  12877  cncfval  12930  bj-indeq  13475  bj-nntrans  13497
 Copyright terms: Public domain W3C validator