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

Theorem ralbii 2673
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 2669 . 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 2649
This theorem is referenced by:  2ralbii  2675  ralinexa  2694  r3al  2706  r19.26-2  2782  r19.26-3  2783  ralbiim  2786  r19.28av  2788  r19.30  2796  r19.32v  2797  r19.35  2798  cbvral2v  2883  cbvral3v  2885  sbralie  2888  ralcom4  2917  reu8  3073  2reuswap  3079  2reu5lem2  3083  eqsn  3903  uni0b  3982  uni0c  3983  ssint  4008  iuniin  4045  iuneq2  4051  iunss  4073  ssiinf  4081  iinab  4093  iinun2  4098  iindif2  4101  iinin2  4102  iinuni  4115  sspwuni  4117  iinpw  4120  disjor  4137  disjxun  4151  dftr3  4247  trint  4258  reusv3  4671  reusv5OLD  4673  reuxfr2d  4686  dfwe2  4702  tfis2f  4775  tfindes  4782  ssrel2  4906  reliun  4935  xpiindi  4950  rexiunxp  4955  ralxpf  4959  rexxpf  4960  dfse2  5177  asymref2  5191  rninxp  5250  dminxp  5251  cnviin  5349  cnvpo  5350  dffun9  5421  funcnv3  5452  fncnv  5455  fnres  5501  fnopabg  5508  mptfng  5510  fint  5562  funimass4  5716  fndmdifeq0  5775  funconstss  5787  f1ompt  5830  idref  5918  dff13f  5945  weniso  6014  foov  6159  frxp  6392  tz7.48lem  6634  tz7.49  6638  oeordi  6766  ixpeq2  7012  ixpin  7023  ixpiin  7024  boxriin  7040  findcard3  7286  fimax2g  7289  fissuni  7346  indexfi  7349  dfsup2  7382  wemapso2lem  7452  zfinf2  7530  oemapso  7571  zfregs2  7602  r1elss  7665  rankc1  7729  cp  7748  bnd2  7750  aceq1  7931  aceq2  7933  kmlem7  7969  kmlem12  7974  kmlem13  7975  kmlem15  7977  fin12  8226  ac6num  8292  ac6s2  8299  ac6sf  8302  ac6s4  8303  zorn2lem4  8312  zorn2lem6  8314  zorn2lem7  8315  zorng  8317  ttukeylem6  8327  brdom7disj  8342  brdom6disj  8343  fpwwe2  8451  fpwwe  8454  axgroth5  8632  axgroth4  8640  grothprim  8642  nqereu  8739  genpnnp  8815  dfinfmr  9917  infmsup  9918  infmrgelb  9920  infmrlb  9921  xrsupsslem  10817  xrinfmsslem  10818  xrinfmss2  10821  fzshftral  11064  hashgt12el  11609  hashgt12el2  11610  hashbc  11629  rexfiuz  12078  clim0  12227  rpnnen2  12752  gcdcllem1  12938  vdwmc2  13274  vdwlem13  13288  vdwnn  13293  xpscf  13718  mreacs  13810  acsfn  13811  acsfn1  13813  acsfn2  13815  ispos2  14332  lubid  14366  oduglb  14493  odulub  14495  posglbd  14503  gsumwspan  14718  isnsg2  14897  oppgid  15079  oppgcntz  15087  efgval2  15283  iscyggen2  15418  iscyg3  15423  oppr1  15666  isnirred  15732  lssne0  15954  isdomn2  16286  iunocv  16831  isbasis2g  16936  basdif0  16941  tgval2  16944  ntreq0  17064  isclo2  17075  opnnei  17107  neiptopnei  17119  lmres  17286  ist1-3  17335  cmpcov2  17375  cmpsub  17385  is1stc2  17426  1stccn  17447  kgencn  17509  eltx  17521  txkgen  17605  fbun  17793  trfbas  17797  fbunfip  17822  trfil2  17840  isufil2  17861  fixufil  17875  hausflim  17934  txflf  17959  fclsopn  17967  alexsubALTlem3  18001  iscau3  19102  iscau4  19103  caucfil  19107  bcth3  19153  ovolgelb  19243  dyadmax  19357  itg2leub  19493  itg2cn  19522  plydivex  20081  vieta1  20096  lgseisenlem2  21001  pnt3  21173  isgrpo2  21633  grpoidinvlem3  21642  nmoubi  22121  lnon0  22147  adjsym  23184  nmopub  23259  nmfnleub  23276  cvbr2  23634  chpssati  23714  chrelat2i  23716  chrelat3  23722  mdsymlem8  23761  ralcom4f  23809  ssiun3  23853  disjorf  23865  mptfnf  23915  ballotlem7  24572  subfacp1lem3  24647  cvmlift2lem1  24768  cvmlift2lem12  24780  untuni  24937  dfso3  24956  dfpo2  25136  setinds  25158  setinds2f  25159  elpotr  25161  dfon2lem7  25169  dfon2lem9  25171  wfis2fg  25235  frins2fg  25271  soseq  25278  axcontlem12  25628  gtinf  26013  filnetlem4  26101  inixp  26121  ac6gf  26125  heibor1lem  26209  heiborlem1  26211  iscrngo2  26299  n0el  26399  ralxpxfr2d  26432  setindtrs  26787  islindf4  26977  r19.32  27613  2rexrsb  27617  cbvral2  27618  2ralbiim  27620  rmoanim  27625  2rmoswap  27630  2reu3  27634  2reu4a  27635  zfregs2VD  28294  bnj110  28567  bnj92  28571  bnj539  28600  bnj540  28601  bnj580  28622  bnj978  28658  bnj1047  28680  bnj1128  28697  bnj1417  28748  bnj1421  28749  bnj1312  28765  bnj1498  28768  lpssat  29128  lssat  29131  lcvbr2  29137  lcvbr3  29138  lfl1  29185  lub0N  29304  glb0N  29308  atlrelat1  29436  hlrelat2  29517  ispsubsp2  29860  pclclN  30005  cdleme25cv  30472  tendoeq2  30888  cdlemk35  31026
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 1661  ax-8 1682  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-ral 2654
  Copyright terms: Public domain W3C validator