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

Theorem ralbii 2299
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 2295 . 2 ( ⊤ → (x A φx A ψ))
43trud 1232 1 (x A φx A ψ)
Colors of variables: wff set class
Syntax hints:  wb 98  wtru 1224  wral 2275
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 1309  ax-gen 1311  ax-4 1373  ax-17 1392
This theorem depends on definitions:  df-bi 110  df-tru 1226  df-nf 1323  df-ral 2280
This theorem is referenced by:  2ralbii  2301  ralinexa  2320  r3al  2335  r19.26-2  2411  r19.26-3  2412  ralbiim  2416  r19.28av  2418  cbvral2v  2510  cbvral3v  2512  sbralie  2515  ralcom4  2544  reu8  2705  2reuswapdc  2711  eqsnm  3489  uni0b  3568  uni0c  3569  ssint  3594  iuniin  3630  iuneq2  3636  iunss  3661  ssiinf  3669  iinab  3681  iindif2m  3687  iinin2m  3688  iinuniss  3700  sspwuni  3702  iinpw  3705  dftr3  3821  trint  3832  bnd2  3889  reusv3  4130  setindel  4193  ordsoexmid  4212  tfi  4220  tfis2f  4222  ssrel2  4345  reliun  4373  xpiindim  4388  ralxpf  4397  dfse2  4613  rninxp  4679  dminxp  4680  cnviinm  4774  cnvpom  4775  cnvsom  4776  dffun9  4844  funco  4854  funcnv3  4875  fncnv  4879  funimaexglem  4896  fnres  4929  fnopabg  4936  mptfng  4938  fintm  4988  f1ompt  5233  idref  5309  dff13f  5322  foov  5558  oacl  5943
  Copyright terms: Public domain W3C validator