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

Theorem ralbii 2330
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 2326 . 2 (⊤ → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
43trud 1252 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1244  wral 2306
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-gen 1338  ax-4 1400  ax-17 1419
This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-ral 2311
This theorem is referenced by:  2ralbii  2332  ralinexa  2351  r3al  2366  r19.26-2  2442  r19.26-3  2443  ralbiim  2447  r19.28av  2449  cbvral2v  2541  cbvral3v  2543  sbralie  2546  ralcom4  2576  reu8  2737  2reuswapdc  2743  eqsnm  3526  uni0b  3605  uni0c  3606  ssint  3631  iuniin  3667  iuneq2  3673  iunss  3698  ssiinf  3706  iinab  3718  iindif2m  3724  iinin2m  3725  iinuniss  3737  sspwuni  3739  iinpw  3742  dftr3  3858  trint  3869  bnd2  3926  reusv3  4192  reg2exmidlema  4259  setindel  4263  ordsoexmid  4286  zfregfr  4298  tfi  4305  tfis2f  4307  ssrel2  4430  reliun  4458  xpiindim  4473  ralxpf  4482  dfse2  4698  rninxp  4764  dminxp  4765  cnviinm  4859  cnvpom  4860  cnvsom  4861  dffun9  4930  funco  4940  funcnv3  4961  fncnv  4965  funimaexglem  4982  fnres  5015  fnopabg  5022  mptfng  5024  fintm  5075  f1ompt  5320  idref  5396  dff13f  5409  foov  5647  oacl  6040  cauappcvgprlemladdrl  6755  axcaucvglemres  6973  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemglsq  9620  resqrexlemsqa  9622  resqrexlemex  9623  clim0  9806
  Copyright terms: Public domain W3C validator