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

Theorem ralbii 2580
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 10 . . 3  |-  (  T. 
->  ( ph  <->  ps )
)
32ralbidv 2576 . 2  |-  (  T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43trud 1314 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    T. wtru 1307   A.wral 2556
This theorem is referenced by:  2ralbii  2582  ralinexa  2601  r3al  2613  r19.26-2  2689  r19.26-3  2690  ralbiim  2693  r19.28av  2695  r19.30  2698  r19.32v  2699  r19.35  2700  cbvral2v  2785  cbvral3v  2787  sbralie  2790  ralcom4  2819  reu8  2974  2reuswap  2980  2reu5lem2  2984  eqsn  3791  uni0b  3868  uni0c  3869  ssint  3894  iuniin  3931  iuneq2  3937  iunss  3959  ssiinf  3967  iinab  3979  iinun2  3984  iindif2  3987  iinin2  3988  iinuni  4001  sspwuni  4003  iinpw  4006  disjor  4023  disjxun  4037  dftr3  4133  trint  4144  reusv3  4558  reusv5OLD  4560  reuxfr2d  4573  dfwe2  4589  tfis2f  4662  tfindes  4669  reliun  4822  xpiindi  4837  rexiunxp  4842  ralxpf  4846  rexxpf  4847  dfse2  5062  asymref2  5076  rninxp  5133  dminxp  5134  cnviin  5228  cnvpo  5229  dffun9  5298  funcnv3  5327  fncnv  5330  fnres  5376  fnopabg  5383  mptfng  5385  fint  5436  funimass4  5589  fndmdifeq0  5647  funconstss  5659  f1ompt  5698  idref  5775  dff13f  5800  weniso  5868  foov  6010  frxp  6241  tz7.48lem  6469  tz7.49  6473  oeordi  6601  ixpeq2  6846  ixpin  6857  ixpiin  6858  boxriin  6874  findcard3  7116  fimax2g  7119  fissuni  7176  indexfi  7179  dfsup2  7211  wemapso2lem  7281  zfinf2  7359  oemapso  7400  zfregs2  7431  r1elss  7494  rankc1  7558  cp  7577  bnd2  7579  aceq1  7760  aceq2  7762  kmlem7  7798  kmlem12  7803  kmlem13  7804  kmlem15  7806  fin12  8055  ac6num  8122  ac9  8126  ac6s2  8129  ac6sf  8132  ac6s4  8133  ac9s  8136  zorn2lem4  8142  zorn2lem6  8144  zorn2lem7  8145  zorng  8147  ttukeylem6  8157  brdom7disj  8172  brdom6disj  8173  fpwwe2  8281  fpwwe  8284  axgroth5  8462  axgroth4  8470  grothprim  8472  nqereu  8569  genpnnp  8645  dfinfmr  9747  infmsup  9748  infmrgelb  9750  infmrlb  9751  xrsupsslem  10641  xrinfmsslem  10642  xrinfmss2  10645  fzshftral  10885  hashbc  11407  rexfiuz  11847  clim0  11996  rpnnen2  12520  gcdcllem1  12706  vdwmc2  13042  vdwlem13  13056  vdwnn  13061  xpscf  13484  mreacs  13576  acsfn  13577  acsfn1  13579  acsfn2  13581  isffth2  13806  ispos2  14098  lubid  14132  oduglb  14259  odulub  14261  posglbd  14269  gsumwspan  14484  isnsg2  14663  oppgid  14845  oppgcntz  14853  efgval2  15049  iscyggen2  15184  iscyg3  15189  oppr1  15432  isnirred  15498  lssne0  15724  isdomn2  16056  iunocv  16597  isbasis2g  16702  basdif0  16707  tgval2  16710  ntreq0  16830  isclo2  16841  opnnei  16873  ordtbaslem  16934  lmres  17044  ist1-3  17093  cmpcov2  17133  cmpsub  17143  is1stc2  17184  1stccn  17205  kgencn  17267  eltx  17279  txkgen  17362  fbun  17551  trfbas  17555  fbunfip  17580  trfil2  17598  isufil2  17619  fixufil  17633  hausflim  17692  txflf  17717  fclsopn  17725  alexsubALTlem3  17759  iscau3  18720  iscau4  18721  caucfil  18725  bcth3  18769  ovolgelb  18855  dyadmax  18969  itg2leub  19105  itg2cn  19134  plydivex  19693  vieta1  19708  lgseisenlem2  20605  pnt3  20777  isgrpo2  20880  grpoidinvlem3  20889  elghom  21046  nmoubi  21366  lnon0  21392  adjsym  22429  nmopub  22504  nmfnleub  22521  cvbr2  22879  chpssati  22959  chrelat2i  22961  chrelat3  22967  mdsymlem8  23006  ballotlem7  23110  ralcom4f  23149  ssiun3  23172  mptfnf  23241  disjorf  23371  subfacp1lem3  23728  cvmlift2lem1  23848  cvmlift2lem12  23860  untuni  24070  dfso3  24089  dfpo2  24183  setinds  24205  setinds2f  24206  elpotr  24208  dfon2lem7  24216  dfon2lem9  24218  wfis2fg  24282  frins2fg  24318  soseq  24325  axcontlem12  24675  negcmpprcal1  25048  negcmpprcal2  25049  domintrefc  25228  dstr  25274  defse3  25375  trinv  25498  vecax3  25558  imonclem  25916  ismonc  25917  isepic  25927  tartarmap  25991  bsstrs  26249  gtinf  26337  filnetlem4  26433  inixp  26502  ac6gf  26514  heibor1lem  26636  heiborlem1  26638  iscrngo2  26726  n0el  26828  ralxpxfr2d  26863  setindtrs  27221  islindf4  27411  r19.32  28048  2rexrsb  28052  cbvral2  28053  2ralbiim  28055  rmoanim  28060  2rmoswap  28065  2reu3  28069  2reu4a  28070  hashgt12el  28218  hashgt12el2  28219  zfregs2VD  28933  bnj110  29206  bnj92  29210  bnj539  29239  bnj540  29240  bnj580  29261  bnj978  29297  bnj1047  29319  bnj1128  29336  bnj1417  29387  bnj1421  29388  bnj1312  29404  bnj1498  29407  lpssat  29825  lssat  29828  lcvbr2  29834  lcvbr3  29835  lfl1  29882  lub0N  30001  glb0N  30005  atlrelat1  30133  hlrelat2  30214  ispsubsp2  30557  pclclN  30702  cdleme25cv  31169  tendoset  31570  tendoeq2  31585  cdlemk35  31723
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1535  df-ral 2561
  Copyright terms: Public domain W3C validator