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

Theorem ralbii 2385
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 2381 . 2 (⊤ → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
43mptru 1299 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 104  wtru 1291  wral 2360
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1382  ax-gen 1384  ax-4 1446  ax-17 1465
This theorem depends on definitions:  df-bi 116  df-tru 1293  df-nf 1396  df-ral 2365
This theorem is referenced by:  2ralbii  2387  ralinexa  2406  r3al  2421  r19.26-2  2499  r19.26-3  2500  ralbiim  2504  r19.28av  2506  cbvral2v  2599  cbvral3v  2601  sbralie  2604  ralcom4  2642  reu8  2812  2reuswapdc  2820  r19.12sn  3512  eqsnm  3605  uni0b  3684  uni0c  3685  ssint  3710  iuniin  3746  iuneq2  3752  iunss  3777  ssiinf  3785  iinab  3797  iindif2m  3803  iinin2m  3804  iinuniss  3817  sspwuni  3819  iinpw  3825  dftr3  3946  trint  3957  bnd2  4014  reusv3  4295  reg2exmidlema  4363  setindel  4367  ordsoexmid  4391  zfregfr  4402  tfi  4410  tfis2f  4412  ssrel2  4541  reliun  4571  xpiindim  4586  ralxpf  4595  dfse2  4818  rninxp  4887  dminxp  4888  cnviinm  4985  cnvpom  4986  cnvsom  4987  dffun9  5057  funco  5067  funcnv3  5089  fncnv  5093  funimaexglem  5110  fnres  5143  fnopabg  5150  mptfng  5152  fintm  5209  f1ompt  5464  idref  5550  dff13f  5563  foov  5805  tfr1onlemaccex  6127  tfrcllembxssdm  6135  tfrcllemaccex  6140  oacl  6235  ixpeq2  6483  ixpin  6494  ixpiinm  6495  infmoti  6777  cauappcvgprlemladdrl  7277  axcaucvglemres  7495  dfinfre  8478  suprzclex  8905  supinfneg  9144  infsupneg  9145  cvg1nlemcau  10478  cvg1nlemres  10479  rexfiuz  10483  recvguniq  10489  resqrexlemglsq  10516  resqrexlemsqa  10518  resqrexlemex  10519  clim0  10734  mertenslem2  10991  infssuzex  11284  bezoutlemmain  11326  isbasis2g  11804  tgval2  11812  ntreq0  11893  decidi  11968  nninfsellemqall  12179  nninfomni  12183
  Copyright terms: Public domain W3C validator