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

Theorem ralbii 2380
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 2376 . 2 (⊤ → (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓))
43trud 1296 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff set class
Syntax hints:  wb 103  wtru 1288  wral 2355
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 1379  ax-gen 1381  ax-4 1443  ax-17 1462
This theorem depends on definitions:  df-bi 115  df-tru 1290  df-nf 1393  df-ral 2360
This theorem is referenced by:  2ralbii  2382  ralinexa  2401  r3al  2416  r19.26-2  2494  r19.26-3  2495  ralbiim  2499  r19.28av  2501  cbvral2v  2594  cbvral3v  2596  sbralie  2599  ralcom4  2635  reu8  2802  2reuswapdc  2808  r19.12sn  3493  eqsnm  3584  uni0b  3663  uni0c  3664  ssint  3689  iuniin  3725  iuneq2  3731  iunss  3756  ssiinf  3764  iinab  3776  iindif2m  3782  iinin2m  3783  iinuniss  3795  sspwuni  3797  iinpw  3800  dftr3  3917  trint  3928  bnd2  3985  reusv3  4258  reg2exmidlema  4325  setindel  4329  ordsoexmid  4353  zfregfr  4364  tfi  4372  tfis2f  4374  ssrel2  4498  reliun  4528  xpiindim  4543  ralxpf  4552  dfse2  4774  rninxp  4842  dminxp  4843  cnviinm  4940  cnvpom  4941  cnvsom  4942  dffun9  5011  funco  5021  funcnv3  5043  fncnv  5047  funimaexglem  5064  fnres  5097  fnopabg  5104  mptfng  5106  fintm  5161  f1ompt  5415  idref  5499  dff13f  5512  foov  5750  tfr1onlemaccex  6069  tfrcllembxssdm  6077  tfrcllemaccex  6082  oacl  6177  infmoti  6670  cauappcvgprlemladdrl  7163  axcaucvglemres  7381  dfinfre  8355  suprzclex  8780  supinfneg  9018  infsupneg  9019  cvg1nlemcau  10334  cvg1nlemres  10335  rexfiuz  10339  recvguniq  10345  resqrexlemglsq  10372  resqrexlemsqa  10374  resqrexlemex  10375  clim0  10589  infssuzex  10870  bezoutlemmain  10912  decidi  11183  nninfsellemqall  11395  nninfomni  11399
  Copyright terms: Public domain W3C validator