ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ralbii Structured version   Unicode 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

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . . 4
21a1i 9 . . 3
32ralbidv 2320 . 2
43trud 1251 1
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  3516  uni0b  3595  uni0c  3596  ssint  3621  iuniin  3657  iuneq2  3663  iunss  3688  ssiinf  3696  iinab  3708  iindif2m  3714  iinin2m  3715  iinuniss  3727  sspwuni  3729  iinpw  3732  dftr3  3848  trint  3859  bnd2  3916  reusv3  4157  setindel  4220  ordsoexmid  4239  tfi  4247  tfis2f  4249  ssrel2  4372  reliun  4400  xpiindim  4415  ralxpf  4424  dfse2  4640  rninxp  4706  dminxp  4707  cnviinm  4801  cnvpom  4802  cnvsom  4803  dffun9  4871  funco  4881  funcnv3  4902  fncnv  4906  funimaexglem  4923  fnres  4956  fnopabg  4963  mptfng  4965  fintm  5016  f1ompt  5261  idref  5337  dff13f  5350  foov  5586  oacl  5972
  Copyright terms: Public domain W3C validator