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

Theorem ralbidva 2408
Description: Formula-building rule for restricted universal quantifier (deduction form). (Contributed by NM, 4-Mar-1997.)
Hypothesis
Ref Expression
ralbidva.1 ((𝜑𝑥𝐴) → (𝜓𝜒))
Assertion
Ref Expression
ralbidva (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Distinct variable group:   𝜑,𝑥
Allowed substitution hints:   𝜓(𝑥)   𝜒(𝑥)   𝐴(𝑥)

Proof of Theorem ralbidva
StepHypRef Expression
1 nfv 1491 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralbida 2406 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104  wcel 1463  wral 2391
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-5 1406  ax-gen 1408  ax-4 1470  ax-17 1489
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-ral 2396
This theorem is referenced by:  raleqbidva  2615  poinxp  4576  funimass4  5438  funimass3  5502  funconstss  5504  cocan1  5654  cocan2  5655  isocnv2  5679  isores2  5680  isoini2  5686  ofrfval  5956  ofrfval2  5964  dfsmo2  6150  smores  6155  smores2  6157  ac6sfi  6758  supisolem  6861  ordiso2  6886  ismkvnex  6995  caucvgsrlemcau  7565  suplocsrlempr  7579  axsuploc  7801  suprleubex  8672  dfinfre  8674  zextlt  9097  prime  9104  fzshftral  9839  fimaxq  10524  clim  11001  clim2  11003  clim2c  11004  clim0c  11006  climabs0  11027  climrecvg1n  11068  mertenslem2  11256  mertensabs  11257  dfgcd2  11609  sqrt2irr  11747  tgss2  12154  neipsm  12229  ssidcn  12285  lmbrf  12290  cnnei  12307  cnrest2  12311  lmss  12321  lmres  12323  ismet2  12429  elmopn2  12524  metss  12569  metrest  12581  metcnp  12587  metcnp2  12588  metcn  12589  txmetcnp  12593  divcnap  12630  elcncf2  12636  mulc1cncf  12651  cncfmet  12654  cdivcncfap  12662  limcdifap  12706  limcmpted  12707  cnlimc  12716
  Copyright terms: Public domain W3C validator