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

Theorem ralbii 2347
Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 23-Nov-1994.) (Revised by Mario Carneiro, 17-Oct-2016.)
Hypothesis
Ref Expression
ralbii.1 (𝜑𝜓)
Assertion
Ref Expression
ralbii (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . . 4 (𝜑𝜓)
21a1i 9 . . 3 (⊤ → (𝜑𝜓))
32ralbidv 2343 . 2 (⊤ → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
43trud 1268 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 102  wtru 1260  wral 2323
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435
This theorem depends on definitions:  df-bi 114  df-tru 1262  df-nf 1366  df-ral 2328
This theorem is referenced by:  2ralbii  2349  ralinexa  2368  r3al  2383  r19.26-2  2459  r19.26-3  2460  ralbiim  2464  r19.28av  2466  cbvral2v  2558  cbvral3v  2560  sbralie  2563  ralcom4  2593  reu8  2760  2reuswapdc  2766  eqsnm  3554  uni0b  3633  uni0c  3634  ssint  3659  iuniin  3695  iuneq2  3701  iunss  3726  ssiinf  3734  iinab  3746  iindif2m  3752  iinin2m  3753  iinuniss  3765  sspwuni  3767  iinpw  3770  dftr3  3886  trint  3897  bnd2  3954  reusv3  4220  reg2exmidlema  4287  setindel  4291  ordsoexmid  4314  zfregfr  4326  tfi  4333  tfis2f  4335  ssrel2  4458  reliun  4486  xpiindim  4501  ralxpf  4510  dfse2  4726  rninxp  4792  dminxp  4793  cnviinm  4887  cnvpom  4888  cnvsom  4889  dffun9  4958  funco  4968  funcnv3  4989  fncnv  4993  funimaexglem  5010  fnres  5043  fnopabg  5050  mptfng  5052  fintm  5103  f1ompt  5348  idref  5424  dff13f  5437  foov  5675  oacl  6071  cauappcvgprlemladdrl  6813  axcaucvglemres  7031  cvg1nlemcau  9811  cvg1nlemres  9812  rexfiuz  9816  recvguniq  9822  resqrexlemglsq  9849  resqrexlemsqa  9851  resqrexlemex  9852  clim0  10037
  Copyright terms: Public domain W3C validator