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

Theorem ralbii 2729
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 2725 . 2  |-  ( T. 
->  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
)
43trud 1371 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   T. wtru 1363   A.wral 2705
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-12 1791
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-ral 2710
This theorem is referenced by:  2ralbii  2731  ralinexa  2750  nrexralim  2752  r3al  2763  r19.26-2  2840  r19.26-3  2841  ralbiim  2844  r19.28av  2846  r19.30  2855  r19.32v  2856  r19.35  2857  cbvral2v  2945  cbvral3v  2947  sbralie  2950  ralcom4  2981  ralxpxfr2d  3073  reu8  3144  2reuswap  3150  2reu5lem2  3154  eqsn  4022  uni0b  4104  uni0c  4105  ssint  4132  iuniin  4169  iuneq2  4175  iunss  4199  ssiinf  4207  iinab  4219  iinun2  4224  iindif2  4227  iinin2  4228  iinuni  4242  sspwuni  4244  iinpw  4247  disjor  4264  disjxun  4278  dftr3  4377  trint  4388  reusv3  4488  reusv5OLD  4490  reuxfr2d  4503  ssrel2  4917  reliun  4947  xpiindi  4962  rexiunxp  4967  ralxpf  4973  rexxpf  4974  dfse2  5190  asymref2  5203  rninxp  5265  dminxp  5266  cnviin  5362  cnvpo  5363  dffun9  5434  funcnv3  5467  fncnv  5470  fnres  5515  fnopabg  5522  mptfng  5524  fint  5578  funimass4  5730  fndmdifeq0  5797  funconstss  5809  f1ompt  5853  idref  5945  dff13f  5960  weniso  6032  foov  6226  dfwe2  6382  tfis2f  6455  tfindes  6462  frxp  6671  tz7.48lem  6882  tz7.49  6886  oeordi  7014  ixpeq2  7265  ixpin  7276  ixpiin  7277  boxriin  7293  findcard3  7543  fimax2g  7546  fissuni  7604  indexfi  7607  dfsup2  7680  wemapsolem  7752  zfinf2  7836  oemapso  7878  zfregs2  7941  r1elss  8001  rankc1  8065  cp  8086  bnd2  8088  aceq1  8275  aceq2  8277  kmlem7  8313  kmlem12  8318  kmlem13  8319  kmlem15  8321  fin12  8570  ac6num  8636  ac6s2  8643  ac6sf  8646  ac6s4  8647  zorn2lem4  8656  zorn2lem6  8658  zorn2lem7  8659  zorng  8661  ttukeylem6  8671  brdom7disj  8686  brdom6disj  8687  fpwwe2  8797  fpwwe  8800  axgroth5  8978  axgroth4  8986  grothprim  8988  nqereu  9085  genpnnp  9161  dfinfmr  10294  infmsup  10295  infmrgelb  10297  infmrlb  10298  xrsupsslem  11256  xrinfmsslem  11257  xrinfmss2  11260  fzshftral  11530  hashgt12el  12156  hashgt12el2  12157  hashbc  12189  rexfiuz  12818  clim0  12967  rpnnen2  13490  gcdcllem1  13677  vdwmc2  14022  vdwlem13  14036  vdwnn  14041  xpscf  14486  mreacs  14578  acsfn  14579  acsfn1  14581  acsfn2  14583  ispos2  15100  lublecllem  15140  oduglb  15291  odulub  15293  posglbd  15302  gsumwspan  15503  isnsg2  15690  oppgid  15850  oppgcntz  15858  efgval2  16200  iscyggen2  16337  iscyg3  16342  oppr1  16659  isnirred  16725  lssne0  16953  isdomn2  17292  iunocv  17947  islindf4  18108  isbasis2g  18394  basdif0  18399  tgval2  18402  ntreq0  18522  isclo2  18533  opnnei  18565  neiptopnei  18577  lmres  18745  ist1-3  18794  cmpcov2  18834  cmpsub  18844  is1stc2  18887  1stccn  18908  kgencn  18970  eltx  18982  txkgen  19066  fbun  19254  trfbas  19258  fbunfip  19283  trfil2  19301  isufil2  19322  fixufil  19336  hausflim  19395  txflf  19420  fclsopn  19428  alexsubALTlem3  19462  iscau3  20630  iscau4  20631  caucfil  20635  bcth3  20683  ovolgelb  20804  dyadmax  20919  itg2leub  21053  itg2cn  21082  plydivex  21647  vieta1  21662  lgseisenlem2  22573  pnt3  22745  axcontlem12  23043  isgrpo2  23506  grpoidinvlem3  23515  nmoubi  23994  lnon0  24020  adjsym  25059  nmopub  25134  nmfnleub  25151  cvbr2  25509  chpssati  25589  chrelat2i  25591  chrelat3  25597  mdsymlem8  25636  ralcom4f  25682  moel  25690  ssiun3  25732  disjnf  25739  disjorf  25746  disjunsn  25759  mptfnf  25799  nn0min  25912  tosglblem  25952  archiabl  26038  eulerpartlems  26590  eulerpartlemr  26604  eulerpartlemn  26611  ballotlem7  26765  subfacp1lem3  26917  cvmlift2lem1  27038  cvmlift2lem12  27050  untuni  27206  dfso3  27222  dfpo2  27411  setinds  27437  setinds2f  27438  elpotr  27440  dfon2lem7  27448  dfon2lem9  27450  wfis2fg  27518  frins2fg  27554  soseq  27561  dfint3  27829  brlb  27832  mblfinlem2  28270  ftc1anc  28316  gtinf  28355  filnetlem4  28443  inixp  28463  ac6gf  28467  heibor1lem  28549  heiborlem1  28551  iscrngo2  28639  ac6s3f  28825  n0el  28846  setindtrs  29216  r19.32  29834  2rexrsb  29838  cbvral2  29839  2ralbiim  29841  rmoanim  29846  2rmoswap  29851  2reu3  29855  2reu4a  29856  ralnralall  29961  raldifsnb  29966  otiunsndisj  29975  otiunsndisjX  29976  dff14b  29988  2spotiundisj  30498  frgrareg  30553  frgraregord013  30554  lindslinindsimp1  30697  lindslinindsimp2  30703  snlindsntor  30711  ldepslinc  30757  zfregs2VD  31276  bnj110  31550  bnj92  31554  bnj539  31583  bnj540  31584  bnj580  31605  bnj978  31641  bnj1047  31663  bnj1128  31680  bnj1417  31731  bnj1421  31732  bnj1312  31748  bnj1498  31751  lpssat  32228  lssat  32231  lcvbr2  32237  lcvbr3  32238  lfl1  32285  lub0N  32404  glb0N  32408  atlrelat1  32536  hlrelat2  32617  ispsubsp2  32960  pclclN  33105  cdleme25cv  33572  tendoeq2  33988  cdlemk35  34126
  Copyright terms: Public domain W3C validator