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

Theorem ralbidva 2376
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 1466 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralbida 2374 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wcel 1438  wral 2359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1381  ax-gen 1383  ax-4 1445  ax-17 1464
This theorem depends on definitions:  df-bi 115  df-nf 1395  df-ral 2364
This theorem is referenced by:  raleqbidva  2576  poinxp  4495  funimass4  5339  funimass3  5399  funconstss  5401  cocan1  5548  cocan2  5549  isocnv2  5573  isores2  5574  isoini2  5580  ofrfval  5846  ofrfval2  5853  dfsmo2  6034  smores  6039  smores2  6041  ac6sfi  6594  supisolem  6682  ordiso2  6707  caucvgsrlemcau  7317  suprleubex  8387  dfinfre  8389  zextlt  8808  prime  8815  fzshftral  9489  fimaxq  10200  clim  10633  clim2  10635  clim2c  10636  clim0c  10638  climabs0  10660  climrecvg1n  10701  dfgcd2  11085  sqrt2irr  11223
  Copyright terms: Public domain W3C validator