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

Theorem ralbii 2818
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  |-  ( ph  <->  ps )
Assertion
Ref Expression
ralbii  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . 3  |-  ( ph  <->  ps )
21imbi2i 314 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2816 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1886   A.wral 2736
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681
This theorem depends on definitions:  df-bi 189  df-ral 2741
This theorem is referenced by:  2ralbii  2819  r3alOLD  2825  dfral2  2834  ralinexa  2838  rexanali  2839  nrexralim  2840  r19.23v  2866  r2exlem  2909  r19.26-2  2917  r19.26-3  2918  ralbiim  2921  r19.28v  2923  r19.30  2934  r19.32v  2935  r19.35  2936  cbvral2v  3026  cbvral3v  3028  sbralie  3031  ralcom4  3065  ralxpxfr2d  3163  reu8  3233  2reuswap  3241  2reu5lem2  3245  r19.12sn  4036  raldifsnb  4102  eqsn  4132  uni0b  4222  uni0c  4223  ssint  4249  iuniin  4288  iuneq2  4294  iunss  4318  ssiinf  4326  iinab  4338  iinun2  4343  iindif2  4346  iinin2  4347  iinuni  4364  sspwuni  4366  iinpw  4369  disjor  4386  disjxun  4399  dftr3  4500  trint  4511  reusv3  4610  reuxfr2d  4622  otiunsndisj  4706  ssrel2  4924  reliun  4953  xpiindi  4969  rexiunxp  4974  ralxpf  4980  rexxpf  4981  dfse2  5201  asymref2  5216  rninxp  5275  dminxp  5276  cnviin  5372  cnvpo  5373  wfis2fg  5416  dffun9  5609  funcnv3  5642  fncnv  5645  fnres  5690  mptfnf  5697  fnopabg  5699  mptfng  5701  fint  5760  funimass4  5914  fndmdifeq0  5986  funconstss  5998  f1ompt  6042  fconstfv  6124  idref  6144  dff13f  6158  dff14b  6169  weniso  6243  foov  6440  dfwe2  6605  tfis2f  6679  tfindes  6686  frxp  6903  tz7.48lem  7155  tz7.49  7159  oeordi  7285  ixpeq2  7533  ixpin  7544  ixpiin  7545  boxriin  7561  findcard3  7811  fimax2g  7814  fissuni  7876  indexfi  7879  dfsup2  7955  sup0riota  7976  infcllem  8000  wemapsolem  8062  zfinf2  8144  oemapso  8184  zfregs2  8214  r1elss  8274  rankc1  8338  cp  8359  bnd2  8361  aceq1  8545  aceq2  8547  kmlem7  8583  kmlem12  8588  kmlem13  8589  kmlem15  8591  fin12  8840  ac6num  8906  ac6s2  8913  ac6sf  8916  ac6s4  8917  zorn2lem4  8926  zorn2lem6  8928  zorn2lem7  8929  zorng  8931  ttukeylem6  8941  brdom7disj  8956  brdom6disj  8957  fpwwe2  9065  fpwwe  9068  axgroth5  9246  axgroth4  9254  grothprim  9256  nqereu  9351  genpnnp  9427  dfinfre  10585  dfinfmrOLD  10586  infrenegsup  10588  infmsupOLD  10589  infmrgelbOLD  10592  infmrlbOLD  10594  xrsupsslem  11589  xrinfmsslem  11590  xrinfmss2  11593  fzshftral  11879  fsuppmapnn0ub  12204  mptnn0fsuppr  12208  hashgt12el  12592  hashgt12el2  12593  hashbc  12613  cotr2g  13033  rexfiuz  13403  clim0  13563  rpnnen2  14271  gcdcllem1  14466  absproddvds  14580  coprmproddvdslem  14672  vdwmc2  14922  vdwlem13  14936  vdwnn  14941  xpscf  15465  mreacs  15557  acsfn  15558  acsfn1  15560  acsfn2  15562  ispos2  16186  lublecllem  16227  oduglb  16378  odulub  16380  posglbd  16389  isnmnd  16533  gsumwspan  16623  isnsg2  16840  oppgid  17000  oppgcntz  17008  efgval2  17367  iscyggen2  17509  iscyg3  17514  oppr1  17855  isnirred  17921  lssne0  18167  isdomn2  18516  iunocv  19237  islindf4  19389  pmatcollpw2lem  19794  isbasis2g  19956  basdif0  19961  tgval2  19964  ntreq0  20086  isclo2  20097  opnnei  20129  neiptopnei  20141  lmres  20309  ist1-3  20358  cmpcov2  20398  cmpsub  20408  is1stc2  20450  1stccn  20471  kgencn  20564  eltx  20576  txkgen  20660  fbun  20848  trfbas  20852  fbunfip  20877  trfil2  20895  isufil2  20916  fixufil  20930  hausflim  20989  txflf  21014  fclsopn  21022  alexsubALTlem3  21057  iscau3  22241  iscau4  22242  caucfil  22246  bcth3  22292  ovolgelb  22426  dyadmax  22549  itg2leub  22685  itg2cn  22714  plydivex  23243  vieta1  23258  lgseisenlem2  24271  pnt3  24443  tglowdim2ln  24689  axcontlem12  24998  2spotiundisj  25783  frgrareg  25838  frgraregord013  25839  isgrpo2  25918  grpoidinvlem3  25927  nmoubi  26406  lnon0  26432  adjsym  27479  nmopub  27554  nmfnleub  27571  cvbr2  27929  chpssati  28009  chrelat2i  28011  chrelat3  28017  mdsymlem8  28056  ralcom4f  28103  moel  28112  uniinn0  28156  ssiun3  28166  disjnf  28174  disjorf  28182  disjunsn  28197  ac6sf2  28219  nn0min  28377  tosglblem  28423  archiabl  28508  eulerpartlems  29186  eulerpartlemr  29200  eulerpartlemn  29207  ballotlem7  29361  ballotlem7OLD  29399  bnj110  29662  bnj92  29666  bnj539  29695  bnj540  29696  bnj580  29717  bnj978  29753  bnj1047  29775  bnj1128  29792  bnj1417  29843  bnj1421  29844  bnj1312  29860  bnj1498  29863  subfacp1lem3  29898  cvmlift2lem1  30018  cvmlift2lem12  30030  untuni  30329  dfso3  30345  dfpo2  30388  setinds  30417  setinds2f  30418  elpotr  30420  dfon2lem7  30428  dfon2lem9  30430  frins2fg  30478  soseq  30485  nosepon  30549  dfint3  30712  brlb  30715  gtinf  30968  filnetlem4  31030  phpreu  31922  ptrecube  31933  poimirlem1  31934  poimirlem25  31958  poimirlem26  31959  poimirlem27  31960  poimirlem30  31963  mblfinlem2  31971  ftc1anc  32018  inixp  32048  ac6gf  32052  heibor1lem  32134  heiborlem1  32136  iscrngo2  32224  ac6s3f  32407  n0el  32427  lpssat  32573  lssat  32576  lcvbr2  32582  lcvbr3  32583  lfl1  32630  lub0N  32749  glb0N  32753  atlrelat1  32881  hlrelat2  32962  ispsubsp2  33305  pclclN  33450  cdleme25cv  33919  tendoeq2  34335  cdlemk35  34473  setindtrs  35874  cllem0  36164  ss2iundf  36245  undisjrab  36648  zfregs2VD  37231  disjinfi  37462  iuneqfzuz  37552  mccl  37672  ioodvbdlimc1lem2  37798  ioodvbdlimc1lem2OLD  37800  ioodvbdlimc2lem  37802  ioodvbdlimc2lemOLD  37803  dvnprodlem3  37817  fourierdlem103  38067  fourierdlem104  38068  sge0iunmpt  38254  hoidmvle  38416  r19.32  38582  2rexrsb  38586  cbvral2  38587  2ralbiim  38589  rmoanim  38594  2rmoswap  38599  2reu3  38603  2reu4a  38604  dfss7  38976  ralnralall  38979  n0snor2el  38990  otiunsndisjX  39000  uhgrvd0nedgb  39528  copisnmnd  39796  lindslinindsimp1  40237  lindslinindsimp2  40243  snlindsntor  40251  ldepslinc  40289  aacllem  40527
  Copyright terms: Public domain W3C validator