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

Theorem ralbii 2895
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 312 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2893 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   A.wral 2814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612
This theorem depends on definitions:  df-bi 185  df-ral 2819
This theorem is referenced by:  2ralbii  2896  r3alOLD  2902  dfral2  2911  ralinexa  2916  rexanali  2917  nrexralim  2918  r19.23v  2943  r2exlem  2982  r19.26-2  2990  r19.26-3  2991  ralbiim  2994  r19.28av  2996  r19.30  3006  r19.32v  3007  r19.35  3008  cbvral2v  3096  cbvral3v  3098  sbralie  3101  ralcom4  3132  ralxpxfr2d  3228  reu8  3299  2reuswap  3306  2reu5lem2  3310  raldifsnb  4158  eqsn  4188  uni0b  4270  uni0c  4271  ssint  4298  iuniin  4336  iuneq2  4342  iunss  4366  ssiinf  4374  iinab  4386  iinun2  4391  iindif2  4394  iinin2  4395  iinuni  4409  sspwuni  4411  iinpw  4414  disjor  4431  disjxun  4445  dftr3  4544  trint  4555  reusv3  4655  reusv5OLD  4657  reuxfr2d  4670  otiunsndisj  4753  ssrel2  5091  reliun  5121  xpiindi  5136  rexiunxp  5141  ralxpf  5147  rexxpf  5148  dfse2  5368  asymref2  5382  rninxp  5444  dminxp  5445  cnviin  5542  cnvpo  5543  dffun9  5614  funcnv3  5647  fncnv  5650  fnres  5695  fnopabg  5702  mptfng  5704  fint  5762  funimass4  5916  fndmdifeq0  5985  funconstss  5997  f1ompt  6041  idref  6139  dff13f  6153  dff14b  6164  weniso  6236  foov  6431  dfwe2  6595  tfis2f  6668  tfindes  6675  frxp  6890  tz7.48lem  7103  tz7.49  7107  oeordi  7233  ixpeq2  7480  ixpin  7491  ixpiin  7492  boxriin  7508  findcard3  7759  fimax2g  7762  fissuni  7821  indexfi  7824  dfsup2  7898  wemapsolem  7971  zfinf2  8055  oemapso  8097  zfregs2  8160  r1elss  8220  rankc1  8284  cp  8305  bnd2  8307  aceq1  8494  aceq2  8496  kmlem7  8532  kmlem12  8537  kmlem13  8538  kmlem15  8540  fin12  8789  ac6num  8855  ac6s2  8862  ac6sf  8865  ac6s4  8866  zorn2lem4  8875  zorn2lem6  8877  zorn2lem7  8878  zorng  8880  ttukeylem6  8890  brdom7disj  8905  brdom6disj  8906  fpwwe2  9017  fpwwe  9020  axgroth5  9198  axgroth4  9206  grothprim  9208  nqereu  9303  genpnnp  9379  dfinfmr  10516  infmsup  10517  infmrgelb  10519  infmrlb  10520  xrsupsslem  11494  xrinfmsslem  11495  xrinfmss2  11498  fzshftral  11761  fsuppmapnn0ub  12065  mptnn0fsuppr  12069  hashgt12el  12442  hashgt12el2  12443  hashbc  12464  rexfiuz  13139  clim0  13288  rpnnen2  13816  gcdcllem1  14004  vdwmc2  14352  vdwlem13  14366  vdwnn  14371  xpscf  14817  mreacs  14909  acsfn  14910  acsfn1  14912  acsfn2  14914  ispos2  15431  lublecllem  15471  oduglb  15622  odulub  15624  posglbd  15633  gsumwspan  15837  isnsg2  16026  oppgid  16186  oppgcntz  16194  efgval2  16538  iscyggen2  16675  iscyg3  16680  oppr1  17067  isnirred  17133  lssne0  17380  isdomn2  17719  iunocv  18479  islindf4  18640  pmatcollpw2lem  19045  isbasis2g  19216  basdif0  19221  tgval2  19224  ntreq0  19344  isclo2  19355  opnnei  19387  neiptopnei  19399  lmres  19567  ist1-3  19616  cmpcov2  19656  cmpsub  19666  is1stc2  19709  1stccn  19730  kgencn  19792  eltx  19804  txkgen  19888  fbun  20076  trfbas  20080  fbunfip  20105  trfil2  20123  isufil2  20144  fixufil  20158  hausflim  20217  txflf  20242  fclsopn  20250  alexsubALTlem3  20284  iscau3  21452  iscau4  21453  caucfil  21457  bcth3  21505  ovolgelb  21626  dyadmax  21742  itg2leub  21876  itg2cn  21905  plydivex  22427  vieta1  22442  lgseisenlem2  23353  pnt3  23525  tglowdim2ln  23745  axcontlem12  23954  2spotiundisj  24739  frgrareg  24794  frgraregord013  24795  isgrpo2  24875  grpoidinvlem3  24884  nmoubi  25363  lnon0  25389  adjsym  26428  nmopub  26503  nmfnleub  26520  cvbr2  26878  chpssati  26958  chrelat2i  26960  chrelat3  26966  mdsymlem8  27005  ralcom4f  27051  moel  27058  ssiun3  27099  disjnf  27106  disjorf  27113  disjunsn  27126  mptfnf  27171  nn0min  27279  tosglblem  27319  archiabl  27404  eulerpartlems  27939  eulerpartlemr  27953  eulerpartlemn  27960  ballotlem7  28114  subfacp1lem3  28266  cvmlift2lem1  28387  cvmlift2lem12  28399  untuni  28556  dfso3  28572  dfpo2  28761  setinds  28787  setinds2f  28788  elpotr  28790  dfon2lem7  28798  dfon2lem9  28800  wfis2fg  28868  frins2fg  28904  soseq  28911  dfint3  29179  brlb  29182  mblfinlem2  29629  ftc1anc  29675  gtinf  29714  filnetlem4  29802  inixp  29822  ac6gf  29826  heibor1lem  29908  heiborlem1  29910  iscrngo2  29998  ac6s3f  30183  n0el  30204  setindtrs  30571  icocncflimc  31228  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  fourierdlem103  31510  fourierdlem104  31511  r19.32  31639  2rexrsb  31643  cbvral2  31644  2ralbiim  31646  rmoanim  31651  2rmoswap  31656  2reu3  31660  2reu4a  31661  ralnralall  31761  otiunsndisjX  31768  lindslinindsimp1  32131  lindslinindsimp2  32137  snlindsntor  32145  ldepslinc  32191  zfregs2VD  32721  bnj110  32995  bnj92  32999  bnj539  33028  bnj540  33029  bnj580  33050  bnj978  33086  bnj1047  33108  bnj1128  33125  bnj1417  33176  bnj1421  33177  bnj1312  33193  bnj1498  33196  lpssat  33810  lssat  33813  lcvbr2  33819  lcvbr3  33820  lfl1  33867  lub0N  33986  glb0N  33990  atlrelat1  34118  hlrelat2  34199  ispsubsp2  34542  pclclN  34687  cdleme25cv  35154  tendoeq2  35570  cdlemk35  35708  cllem0  36771
  Copyright terms: Public domain W3C validator