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

Theorem ralbii 2690
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  |-  ( 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 . . . 4  |-  ( ph  <->  ps )
21a1i 11 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32ralbidv 2686 . 2  |-  (  T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43trud 1329 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    T. wtru 1322   A.wral 2666
This theorem is referenced by:  2ralbii  2692  ralinexa  2711  r3al  2723  r19.26-2  2799  r19.26-3  2800  ralbiim  2803  r19.28av  2805  r19.30  2813  r19.32v  2814  r19.35  2815  cbvral2v  2900  cbvral3v  2902  sbralie  2905  ralcom4  2934  reu8  3090  2reuswap  3096  2reu5lem2  3100  eqsn  3920  uni0b  4000  uni0c  4001  ssint  4026  iuniin  4063  iuneq2  4069  iunss  4092  ssiinf  4100  iinab  4112  iinun2  4117  iindif2  4120  iinin2  4121  iinuni  4134  sspwuni  4136  iinpw  4139  disjor  4156  disjxun  4170  dftr3  4266  trint  4277  reusv3  4690  reusv5OLD  4692  reuxfr2d  4705  dfwe2  4721  tfis2f  4794  tfindes  4801  ssrel2  4925  reliun  4954  xpiindi  4969  rexiunxp  4974  ralxpf  4978  rexxpf  4979  dfse2  5196  asymref2  5210  rninxp  5269  dminxp  5270  cnviin  5368  cnvpo  5369  dffun9  5440  funcnv3  5471  fncnv  5474  fnres  5520  fnopabg  5527  mptfng  5529  fint  5581  funimass4  5736  fndmdifeq0  5795  funconstss  5807  f1ompt  5850  idref  5938  dff13f  5965  weniso  6034  foov  6179  frxp  6415  tz7.48lem  6657  tz7.49  6661  oeordi  6789  ixpeq2  7035  ixpin  7046  ixpiin  7047  boxriin  7063  findcard3  7309  fimax2g  7312  fissuni  7369  indexfi  7372  dfsup2  7405  wemapso2lem  7475  zfinf2  7553  oemapso  7594  zfregs2  7625  r1elss  7688  rankc1  7752  cp  7771  bnd2  7773  aceq1  7954  aceq2  7956  kmlem7  7992  kmlem12  7997  kmlem13  7998  kmlem15  8000  fin12  8249  ac6num  8315  ac6s2  8322  ac6sf  8325  ac6s4  8326  zorn2lem4  8335  zorn2lem6  8337  zorn2lem7  8338  zorng  8340  ttukeylem6  8350  brdom7disj  8365  brdom6disj  8366  fpwwe2  8474  fpwwe  8477  axgroth5  8655  axgroth4  8663  grothprim  8665  nqereu  8762  genpnnp  8838  dfinfmr  9941  infmsup  9942  infmrgelb  9944  infmrlb  9945  xrsupsslem  10841  xrinfmsslem  10842  xrinfmss2  10845  fzshftral  11089  hashgt12el  11637  hashgt12el2  11638  hashbc  11657  rexfiuz  12106  clim0  12255  rpnnen2  12780  gcdcllem1  12966  vdwmc2  13302  vdwlem13  13316  vdwnn  13321  xpscf  13746  mreacs  13838  acsfn  13839  acsfn1  13841  acsfn2  13843  ispos2  14360  lubid  14394  oduglb  14521  odulub  14523  posglbd  14531  gsumwspan  14746  isnsg2  14925  oppgid  15107  oppgcntz  15115  efgval2  15311  iscyggen2  15446  iscyg3  15451  oppr1  15694  isnirred  15760  lssne0  15982  isdomn2  16314  iunocv  16863  isbasis2g  16968  basdif0  16973  tgval2  16976  ntreq0  17096  isclo2  17107  opnnei  17139  neiptopnei  17151  lmres  17318  ist1-3  17367  cmpcov2  17407  cmpsub  17417  is1stc2  17458  1stccn  17479  kgencn  17541  eltx  17553  txkgen  17637  fbun  17825  trfbas  17829  fbunfip  17854  trfil2  17872  isufil2  17893  fixufil  17907  hausflim  17966  txflf  17991  fclsopn  17999  alexsubALTlem3  18033  iscau3  19184  iscau4  19185  caucfil  19189  bcth3  19237  ovolgelb  19329  dyadmax  19443  itg2leub  19579  itg2cn  19608  plydivex  20167  vieta1  20182  lgseisenlem2  21087  pnt3  21259  isgrpo2  21738  grpoidinvlem3  21747  nmoubi  22226  lnon0  22252  adjsym  23289  nmopub  23364  nmfnleub  23381  cvbr2  23739  chpssati  23819  chrelat2i  23821  chrelat3  23827  mdsymlem8  23866  ralcom4f  23918  ssiun3  23962  disjorf  23974  mptfnf  24026  tosglb  24145  ballotlem7  24746  subfacp1lem3  24821  cvmlift2lem1  24942  cvmlift2lem12  24954  untuni  25111  dfso3  25130  dfpo2  25326  setinds  25348  setinds2f  25349  elpotr  25351  dfon2lem7  25359  dfon2lem9  25361  wfis2fg  25425  frins2fg  25461  soseq  25468  axcontlem12  25818  mblfinlem  26143  gtinf  26212  filnetlem4  26300  inixp  26320  ac6gf  26324  heibor1lem  26408  heiborlem1  26410  iscrngo2  26498  n0el  26598  ralxpxfr2d  26631  setindtrs  26986  islindf4  27176  r19.32  27812  2rexrsb  27816  cbvral2  27817  2ralbiim  27819  rmoanim  27824  2rmoswap  27829  2reu3  27833  2reu4a  27834  raldifsnb  27946  otiunsndisj  27954  otiunsndisjX  27955  dff14b  27960  2spotiundisj  28165  zfregs2VD  28662  bnj110  28935  bnj92  28939  bnj539  28968  bnj540  28969  bnj580  28990  bnj978  29026  bnj1047  29048  bnj1128  29065  bnj1417  29116  bnj1421  29117  bnj1312  29133  bnj1498  29136  lpssat  29496  lssat  29499  lcvbr2  29505  lcvbr3  29506  lfl1  29553  lub0N  29672  glb0N  29676  atlrelat1  29804  hlrelat2  29885  ispsubsp2  30228  pclclN  30373  cdleme25cv  30840  tendoeq2  31256  cdlemk35  31394
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-ral 2671
  Copyright terms: Public domain W3C validator