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

Theorem ralbidva 2486
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 1539 . 2 𝑥𝜑
2 ralbidva.1 . 2 ((𝜑𝑥𝐴) → (𝜓𝜒))
31, 2ralbida 2484 1 (𝜑 → (∀𝑥𝐴 𝜓 ↔ ∀𝑥𝐴 𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105  wcel 2160  wral 2468
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1458  ax-gen 1460  ax-4 1521  ax-17 1537
This theorem depends on definitions:  df-bi 117  df-nf 1472  df-ral 2473
This theorem is referenced by:  raleqbidva  2700  poinxp  4713  funimass4  5587  fnmptfvd  5641  funimass3  5653  funconstss  5655  cocan1  5809  cocan2  5810  isocnv2  5834  isores2  5835  isoini2  5841  ofrfval  6116  ofrfval2  6124  dfsmo2  6313  smores  6318  smores2  6320  ac6sfi  6927  supisolem  7038  ordiso2  7065  ismkvnex  7184  nninfwlporlemd  7201  caucvgsrlemcau  7823  suplocsrlempr  7837  axsuploc  8061  suprleubex  8942  dfinfre  8944  zextlt  9376  prime  9383  infregelbex  9630  fzshftral  10140  fimaxq  10842  clim  11324  clim2  11326  clim2c  11327  clim0c  11329  climabs0  11350  climrecvg1n  11391  mertenslem2  11579  mertensabs  11580  dfgcd2  12050  sqrt2irr  12197  pc11  12366  pcz  12367  1arith  12402  infpn2  12510  grpidpropdg  12853  sgrppropd  12891  mndpropd  12916  grppropd  12977  issubg4m  13149  rngpropd  13326  ringpropd  13409  oppr1g  13449  lsspropdg  13764  isridlrng  13815  isridl  13836  tgss2  14056  neipsm  14131  ssidcn  14187  lmbrf  14192  cnnei  14209  cnrest2  14213  lmss  14223  lmres  14225  ismet2  14331  elmopn2  14426  metss  14471  metrest  14483  metcnp  14489  metcnp2  14490  metcn  14491  txmetcnp  14495  divcnap  14532  elcncf2  14538  mulc1cncf  14553  cncfmet  14556  cdivcncfap  14564  limcdifap  14608  limcmpted  14609  cnlimc  14618  2sqlem6  14945  iswomni0  15278  cndcap  15286
  Copyright terms: Public domain W3C validator