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

Theorem ralbii 2324
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 (x A φx A ψ)

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . . 4 (φψ)
21a1i 9 . . 3 ( ⊤ → (φψ))
32ralbidv 2320 . 2 ( ⊤ → (x A φx A ψ))
43trud 1251 1 (x A φx A ψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1243  wral 2300
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 1333  ax-gen 1335  ax-4 1397  ax-17 1416
This theorem depends on definitions:  df-bi 110  df-tru 1245  df-nf 1347  df-ral 2305
This theorem is referenced by:  2ralbii  2326  ralinexa  2345  r3al  2360  r19.26-2  2436  r19.26-3  2437  ralbiim  2441  r19.28av  2443  cbvral2v  2535  cbvral3v  2537  sbralie  2540  ralcom4  2570  reu8  2731  2reuswapdc  2737  eqsnm  3517  uni0b  3596  uni0c  3597  ssint  3622  iuniin  3658  iuneq2  3664  iunss  3689  ssiinf  3697  iinab  3709  iindif2m  3715  iinin2m  3716  iinuniss  3728  sspwuni  3730  iinpw  3733  dftr3  3849  trint  3860  bnd2  3917  reusv3  4158  setindel  4221  ordsoexmid  4240  tfi  4248  tfis2f  4250  ssrel2  4373  reliun  4401  xpiindim  4416  ralxpf  4425  dfse2  4641  rninxp  4707  dminxp  4708  cnviinm  4802  cnvpom  4803  cnvsom  4804  dffun9  4873  funco  4883  funcnv3  4904  fncnv  4908  funimaexglem  4925  fnres  4958  fnopabg  4965  mptfng  4967  fintm  5018  f1ompt  5263  idref  5339  dff13f  5352  foov  5589  oacl  5979  cauappcvgprlemladdrl  6628
  Copyright terms: Public domain W3C validator