MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ralbii Unicode version

Theorem ralbii 2888
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.) (Proof shortened by Wolf Lammen, 4-Dec-2019.)
Hypothesis
Ref Expression
ralbii.1
Assertion
Ref Expression
ralbii

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . 3
21imbi2i 312 . 2
32ralbii2 2886 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818  A.wral 2807
This theorem is referenced by:  2ralbii  2889  r3alOLD  2895  dfral2  2904  ralinexa  2909  rexanali  2910  nrexralim  2911  r19.23v  2937  r2exlem  2977  r19.26-2  2985  r19.26-3  2986  ralbiim  2989  r19.28v  2991  r19.30  3002  r19.32v  3003  r19.35  3004  cbvral2v  3092  cbvral3v  3094  sbralie  3097  ralcom4  3128  ralxpxfr2d  3224  reu8  3295  2reuswap  3302  2reu5lem2  3306  r19.12sn  4095  raldifsnb  4161  eqsn  4191  uni0b  4274  uni0c  4275  ssint  4302  iuniin  4341  iuneq2  4347  iunss  4371  ssiinf  4379  iinab  4391  iinun2  4396  iindif2  4399  iinin2  4400  iinuni  4414  sspwuni  4416  iinpw  4419  disjor  4436  disjxun  4450  dftr3  4549  trint  4560  reusv3  4660  reusv5OLD  4662  reuxfr2d  4675  otiunsndisj  4758  ssrel2  5098  reliun  5128  xpiindi  5143  rexiunxp  5148  ralxpf  5154  rexxpf  5155  dfse2  5375  asymref2  5389  rninxp  5451  dminxp  5452  cnviin  5549  cnvpo  5550  dffun9  5621  funcnv3  5654  fncnv  5657  fnres  5702  fnopabg  5709  mptfng  5711  fint  5769  funimass4  5924  fndmdifeq0  5993  funconstss  6005  f1ompt  6053  fconstfv  6133  idref  6153  dff13f  6167  dff14b  6178  weniso  6250  foov  6449  dfwe2  6617  tfis2f  6690  tfindes  6697  frxp  6910  tz7.48lem  7125  tz7.49  7129  oeordi  7255  ixpeq2  7503  ixpin  7514  ixpiin  7515  boxriin  7531  findcard3  7783  fimax2g  7786  fissuni  7845  indexfi  7848  dfsup2  7922  wemapsolem  7996  zfinf2  8080  oemapso  8122  zfregs2  8185  r1elss  8245  rankc1  8309  cp  8330  bnd2  8332  aceq1  8519  aceq2  8521  kmlem7  8557  kmlem12  8562  kmlem13  8563  kmlem15  8565  fin12  8814  ac6num  8880  ac6s2  8887  ac6sf  8890  ac6s4  8891  zorn2lem4  8900  zorn2lem6  8902  zorn2lem7  8903  zorng  8905  ttukeylem6  8915  brdom7disj  8930  brdom6disj  8931  fpwwe2  9042  fpwwe  9045  axgroth5  9223  axgroth4  9231  grothprim  9233  nqereu  9328  genpnnp  9404  dfinfmr  10545  infmsup  10546  infmrgelb  10548  infmrlb  10549  xrsupsslem  11527  xrinfmsslem  11528  xrinfmss2  11531  fzshftral  11795  fsuppmapnn0ub  12101  mptnn0fsuppr  12105  hashgt12el  12481  hashgt12el2  12482  hashbc  12502  rexfiuz  13180  clim0  13329  rpnnen2  13959  gcdcllem1  14149  vdwmc2  14497  vdwlem13  14511  vdwnn  14516  xpscf  14963  mreacs  15055  acsfn  15056  acsfn1  15058  acsfn2  15060  ispos2  15577  lublecllem  15618  oduglb  15769  odulub  15771  posglbd  15780  isnmnd  15924  gsumwspan  16014  isnsg2  16231  oppgid  16391  oppgcntz  16399  efgval2  16742  iscyggen2  16884  iscyg3  16889  oppr1  17283  isnirred  17349  lssne0  17597  isdomn2  17948  iunocv  18712  islindf4  18873  pmatcollpw2lem  19278  isbasis2g  19449  basdif0  19454  tgval2  19457  ntreq0  19578  isclo2  19589  opnnei  19621  neiptopnei  19633  lmres  19801  ist1-3  19850  cmpcov2  19890  cmpsub  19900  is1stc2  19943  1stccn  19964  kgencn  20057  eltx  20069  txkgen  20153  fbun  20341  trfbas  20345  fbunfip  20370  trfil2  20388  isufil2  20409  fixufil  20423  hausflim  20482  txflf  20507  fclsopn  20515  alexsubALTlem3  20549  iscau3  21717  iscau4  21718  caucfil  21722  bcth3  21770  ovolgelb  21891  dyadmax  22007  itg2leub  22141  itg2cn  22170  plydivex  22693  vieta1  22708  lgseisenlem2  23625  pnt3  23797  tglowdim2ln  24032  axcontlem12  24278  2spotiundisj  25062  frgrareg  25117  frgraregord013  25118  isgrpo2  25199  grpoidinvlem3  25208  nmoubi  25687  lnon0  25713  adjsym  26752  nmopub  26827  nmfnleub  26844  cvbr2  27202  chpssati  27282  chrelat2i  27284  chrelat3  27290  mdsymlem8  27329  ralcom4f  27375  moel  27382  uniinn0  27424  ssiun3  27426  disjnf  27433  disjorf  27440  disjunsn  27453  mptfnf  27499  nn0min  27611  tosglblem  27657  archiabl  27742  eulerpartlems  28299  eulerpartlemr  28313  eulerpartlemn  28320  ballotlem7  28474  subfacp1lem3  28626  cvmlift2lem1  28747  cvmlift2lem12  28759  untuni  29081  dfso3  29097  dfpo2  29184  setinds  29210  setinds2f  29211  elpotr  29213  dfon2lem7  29221  dfon2lem9  29223  wfis2fg  29291  frins2fg  29327  soseq  29334  dfint3  29602  brlb  29605  mblfinlem2  30052  ftc1anc  30098  gtinf  30137  filnetlem4  30199  inixp  30219  ac6gf  30223  heibor1lem  30305  heiborlem1  30307  iscrngo2  30395  ac6s3f  30579  n0el  30600  setindtrs  30967  undisjrab  31186  mccl  31606  ioodvbdlimc1lem2  31729  ioodvbdlimc2lem  31731  dvnprodlem3  31745  fourierdlem103  31992  fourierdlem104  31993  r19.32  32172  2rexrsb  32176  cbvral2  32177  2ralbiim  32179  rmoanim  32184  2rmoswap  32189  2reu3  32193  2reu4a  32194  ralnralall  32294  otiunsndisjX  32301  copisnmnd  32497  lindslinindsimp1  33058  lindslinindsimp2  33064  snlindsntor  33072  ldepslinc  33110  aacllem  33216  zfregs2VD  33641  bnj110  33916  bnj92  33920  bnj539  33949  bnj540  33950  bnj580  33971  bnj978  34007  bnj1047  34029  bnj1128  34046  bnj1417  34097  bnj1421  34098  bnj1312  34114  bnj1498  34117  lpssat  34738  lssat  34741  lcvbr2  34747  lcvbr3  34748  lfl1  34795  lub0N  34914  glb0N  34918  atlrelat1  35046  hlrelat2  35127  ispsubsp2  35470  pclclN  35615  cdleme25cv  36084  tendoeq2  36500  cdlemk35  36638  cllem0  37751  cotr2g  37786
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631
This theorem depends on definitions:  df-bi 185  df-ral 2812
  Copyright terms: Public domain W3C validator