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

Theorem ralbii 2567
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 2563 . 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 2543
This theorem is referenced by:  2ralbii  2569  ralinexa  2588  r3al  2600  r19.26-2  2676  r19.26-3  2677  ralbiim  2680  r19.28av  2682  r19.30  2685  r19.32v  2686  r19.35  2687  cbvral2v  2772  cbvral3v  2774  sbralie  2777  ralcom4  2806  reu8  2961  2reuswap  2967  2reu5lem2  2971  eqsn  3775  uni0b  3852  uni0c  3853  ssint  3878  iuniin  3915  iuneq2  3921  iunss  3943  ssiinf  3951  iinab  3963  iinun2  3968  iindif2  3971  iinin2  3972  iinuni  3985  sspwuni  3987  iinpw  3990  disjor  4007  disjxun  4021  dftr3  4117  trint  4128  reusv3  4542  reusv5OLD  4544  reuxfr2d  4557  dfwe2  4573  tfis2f  4646  tfindes  4653  reliun  4806  xpiindi  4821  rexiunxp  4826  ralxpf  4830  rexxpf  4831  dfse2  5046  asymref2  5060  rninxp  5117  dminxp  5118  cnviin  5212  cnvpo  5213  dffun9  5282  funcnv3  5311  fncnv  5314  fnres  5360  fnopabg  5367  mptfng  5369  fint  5420  funimass4  5573  fndmdifeq0  5631  funconstss  5643  f1ompt  5682  idref  5759  dff13f  5784  weniso  5852  foov  5994  frxp  6225  tz7.48lem  6453  tz7.49  6457  oeordi  6585  ixpeq2  6830  ixpin  6841  ixpiin  6842  boxriin  6858  findcard3  7100  fimax2g  7103  fissuni  7160  indexfi  7163  dfsup2  7195  wemapso2lem  7265  zfinf2  7343  oemapso  7384  zfregs2  7415  r1elss  7478  rankc1  7542  cp  7561  bnd2  7563  aceq1  7744  aceq2  7746  kmlem7  7782  kmlem12  7787  kmlem13  7788  kmlem15  7790  fin12  8039  ac6num  8106  ac9  8110  ac6s2  8113  ac6sf  8116  ac6s4  8117  ac9s  8120  zorn2lem4  8126  zorn2lem6  8128  zorn2lem7  8129  zorng  8131  ttukeylem6  8141  brdom7disj  8156  brdom6disj  8157  fpwwe2  8265  fpwwe  8268  axgroth5  8446  axgroth4  8454  grothprim  8456  nqereu  8553  genpnnp  8629  dfinfmr  9731  infmsup  9732  infmrgelb  9734  infmrlb  9735  xrsupsslem  10625  xrinfmsslem  10626  xrinfmss2  10629  fzshftral  10869  hashbc  11391  rexfiuz  11831  clim0  11980  rpnnen2  12504  gcdcllem1  12690  vdwmc2  13026  vdwlem13  13040  vdwnn  13045  xpscf  13468  mreacs  13560  acsfn  13561  acsfn1  13563  acsfn2  13565  isffth2  13790  ispos2  14082  lubid  14116  oduglb  14243  odulub  14245  posglbd  14253  gsumwspan  14468  isnsg2  14647  oppgid  14829  oppgcntz  14837  efgval2  15033  iscyggen2  15168  iscyg3  15173  oppr1  15416  isnirred  15482  lssne0  15708  isdomn2  16040  iunocv  16581  isbasis2g  16686  basdif0  16691  tgval2  16694  ntreq0  16814  isclo2  16825  opnnei  16857  ordtbaslem  16918  lmres  17028  ist1-3  17077  cmpcov2  17117  cmpsub  17127  is1stc2  17168  1stccn  17189  kgencn  17251  eltx  17263  txkgen  17346  fbun  17535  trfbas  17539  fbunfip  17564  trfil2  17582  isufil2  17603  fixufil  17617  hausflim  17676  txflf  17701  fclsopn  17709  alexsubALTlem3  17743  iscau3  18704  iscau4  18705  caucfil  18709  bcth3  18753  ovolgelb  18839  dyadmax  18953  itg2leub  19089  itg2cn  19118  plydivex  19677  vieta1  19692  lgseisenlem2  20589  pnt3  20761  isgrpo2  20864  grpoidinvlem3  20873  elghom  21030  nmoubi  21350  lnon0  21376  adjsym  22413  nmopub  22488  nmfnleub  22505  cvbr2  22863  chpssati  22943  chrelat2i  22945  chrelat3  22951  mdsymlem8  22990  ballotlem7  23094  ralcom4f  23133  ssiun3  23156  mptfnf  23226  disjorf  23356  subfacp1lem3  23713  cvmlift2lem1  23833  cvmlift2lem12  23845  untuni  24055  dfso3  24074  dfpo2  24112  setinds  24134  setinds2f  24135  elpotr  24137  dfon2lem7  24145  dfon2lem9  24147  wfis2fg  24211  frins2fg  24247  soseq  24254  axcontlem12  24603  negcmpprcal1  24945  negcmpprcal2  24946  domintrefc  25125  dstr  25171  defse3  25272  trinv  25395  vecax3  25455  imonclem  25813  ismonc  25814  isepic  25824  tartarmap  25888  bsstrs  26146  gtinf  26234  filnetlem4  26330  inixp  26399  ac6gf  26411  heibor1lem  26533  heiborlem1  26535  iscrngo2  26623  n0el  26725  ralxpxfr2d  26760  setindtrs  27118  islindf4  27308  r19.32  27945  2rexrsb  27949  cbvral2  27950  2ralbiim  27952  rmoanim  27957  2rmoswap  27962  2reu3  27966  2reu4a  27967  zfregs2VD  28617  bnj110  28890  bnj92  28894  bnj539  28923  bnj540  28924  bnj580  28945  bnj978  28981  bnj1047  29003  bnj1128  29020  bnj1417  29071  bnj1421  29072  bnj1312  29088  bnj1498  29091  lpssat  29203  lssat  29206  lcvbr2  29212  lcvbr3  29213  lfl1  29260  lub0N  29379  glb0N  29383  atlrelat1  29511  hlrelat2  29592  ispsubsp2  29935  pclclN  30080  cdleme25cv  30547  tendoset  30948  tendoeq2  30963  cdlemk35  31101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-nf 1532  df-ral 2548
  Copyright terms: Public domain W3C validator