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

Theorem ralbii 2857
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.) (Proof shortened by Wolf Lammen, 4-Dec-2019.)
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 . . 3  |-  ( ph  <->  ps )
21imbi2i 314 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2855 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1869   A.wral 2776
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679
This theorem depends on definitions:  df-bi 189  df-ral 2781
This theorem is referenced by:  2ralbii  2858  r3alOLD  2864  dfral2  2873  ralinexa  2878  rexanali  2879  nrexralim  2880  r19.23v  2906  r2exlem  2949  r19.26-2  2957  r19.26-3  2958  ralbiim  2961  r19.28v  2963  r19.30  2974  r19.32v  2975  r19.35  2976  cbvral2v  3064  cbvral3v  3066  sbralie  3069  ralcom4  3101  ralxpxfr2d  3197  reu8  3268  2reuswap  3275  2reu5lem2  3279  r19.12sn  4063  raldifsnb  4129  eqsn  4159  uni0b  4242  uni0c  4243  ssint  4269  iuniin  4308  iuneq2  4314  iunss  4338  ssiinf  4346  iinab  4358  iinun2  4363  iindif2  4366  iinin2  4367  iinuni  4384  sspwuni  4386  iinpw  4389  disjor  4406  disjxun  4419  dftr3  4520  trint  4531  reusv3  4630  reuxfr2d  4642  otiunsndisj  4724  ssrel2  4942  reliun  4971  xpiindi  4987  rexiunxp  4992  ralxpf  4998  rexxpf  4999  dfse2  5219  asymref2  5234  rninxp  5293  dminxp  5294  cnviin  5390  cnvpo  5391  wfis2fg  5434  dffun9  5627  funcnv3  5660  fncnv  5663  fnres  5708  mptfnf  5715  fnopabg  5717  mptfng  5719  fint  5777  funimass4  5930  fndmdifeq0  6001  funconstss  6013  f1ompt  6057  fconstfv  6139  idref  6159  dff13f  6173  dff14b  6184  weniso  6258  foov  6455  dfwe2  6620  tfis2f  6694  tfindes  6701  frxp  6915  tz7.48lem  7164  tz7.49  7168  oeordi  7294  ixpeq2  7542  ixpin  7553  ixpiin  7554  boxriin  7570  findcard3  7818  fimax2g  7821  fissuni  7883  indexfi  7886  dfsup2  7962  sup0riota  7983  infcllem  8007  wemapsolem  8069  zfinf2  8151  oemapso  8190  zfregs2  8220  r1elss  8280  rankc1  8344  cp  8365  bnd2  8367  aceq1  8550  aceq2  8552  kmlem7  8588  kmlem12  8593  kmlem13  8594  kmlem15  8596  fin12  8845  ac6num  8911  ac6s2  8918  ac6sf  8921  ac6s4  8922  zorn2lem4  8931  zorn2lem6  8933  zorn2lem7  8934  zorng  8936  ttukeylem6  8946  brdom7disj  8961  brdom6disj  8962  fpwwe2  9070  fpwwe  9073  axgroth5  9251  axgroth4  9259  grothprim  9261  nqereu  9356  genpnnp  9432  dfinfre  10590  dfinfmrOLD  10591  infrenegsup  10593  infmsupOLD  10594  infmrgelbOLD  10597  infmrlbOLD  10599  xrsupsslem  11594  xrinfmsslem  11595  xrinfmss2  11598  fzshftral  11884  fsuppmapnn0ub  12208  mptnn0fsuppr  12212  hashgt12el  12594  hashgt12el2  12595  hashbc  12615  cotr2g  13034  rexfiuz  13404  clim0  13563  rpnnen2  14271  gcdcllem1  14466  absproddvds  14580  coprmproddvdslem  14672  vdwmc2  14922  vdwlem13  14936  vdwnn  14941  xpscf  15465  mreacs  15557  acsfn  15558  acsfn1  15560  acsfn2  15562  ispos2  16186  lublecllem  16227  oduglb  16378  odulub  16380  posglbd  16389  isnmnd  16533  gsumwspan  16623  isnsg2  16840  oppgid  17000  oppgcntz  17008  efgval2  17367  iscyggen2  17509  iscyg3  17514  oppr1  17855  isnirred  17921  lssne0  18167  isdomn2  18516  iunocv  19236  islindf4  19388  pmatcollpw2lem  19793  isbasis2g  19955  basdif0  19960  tgval2  19963  ntreq0  20085  isclo2  20096  opnnei  20128  neiptopnei  20140  lmres  20308  ist1-3  20357  cmpcov2  20397  cmpsub  20407  is1stc2  20449  1stccn  20470  kgencn  20563  eltx  20575  txkgen  20659  fbun  20847  trfbas  20851  fbunfip  20876  trfil2  20894  isufil2  20915  fixufil  20929  hausflim  20988  txflf  21013  fclsopn  21021  alexsubALTlem3  21056  iscau3  22240  iscau4  22241  caucfil  22245  bcth3  22291  ovolgelb  22425  dyadmax  22548  itg2leub  22684  itg2cn  22713  plydivex  23242  vieta1  23257  lgseisenlem2  24270  pnt3  24442  tglowdim2ln  24688  axcontlem12  24997  2spotiundisj  25782  frgrareg  25837  frgraregord013  25838  isgrpo2  25917  grpoidinvlem3  25926  nmoubi  26405  lnon0  26431  adjsym  27478  nmopub  27553  nmfnleub  27570  cvbr2  27928  chpssati  28008  chrelat2i  28010  chrelat3  28016  mdsymlem8  28055  ralcom4f  28102  moel  28111  uniinn0  28159  ssiun3  28169  disjnf  28177  disjorf  28185  disjunsn  28200  ac6sf2  28222  nn0min  28385  tosglblem  28431  archiabl  28516  eulerpartlems  29195  eulerpartlemr  29209  eulerpartlemn  29216  ballotlem7  29370  ballotlem7OLD  29408  bnj110  29671  bnj92  29675  bnj539  29704  bnj540  29705  bnj580  29726  bnj978  29762  bnj1047  29784  bnj1128  29801  bnj1417  29852  bnj1421  29853  bnj1312  29869  bnj1498  29872  subfacp1lem3  29907  cvmlift2lem1  30027  cvmlift2lem12  30039  untuni  30338  dfso3  30354  dfpo2  30396  setinds  30425  setinds2f  30426  elpotr  30428  dfon2lem7  30436  dfon2lem9  30438  frins2fg  30486  soseq  30493  dfint3  30718  brlb  30721  gtinf  30974  filnetlem4  31036  phpreu  31887  ptrecube  31898  poimirlem1  31899  poimirlem25  31923  poimirlem26  31924  poimirlem27  31925  poimirlem30  31928  mblfinlem2  31936  ftc1anc  31983  inixp  32013  ac6gf  32017  heibor1lem  32099  heiborlem1  32101  iscrngo2  32189  ac6s3f  32372  n0el  32393  lpssat  32542  lssat  32545  lcvbr2  32551  lcvbr3  32552  lfl1  32599  lub0N  32718  glb0N  32722  atlrelat1  32850  hlrelat2  32931  ispsubsp2  33274  pclclN  33419  cdleme25cv  33888  tendoeq2  34304  cdlemk35  34442  setindtrs  35844  cllem0  36134  ss2iundf  36155  undisjrab  36556  zfregs2VD  37142  disjinfi  37362  iuneqfzuz  37444  mccl  37542  ioodvbdlimc1lem2  37668  ioodvbdlimc1lem2OLD  37670  ioodvbdlimc2lem  37672  ioodvbdlimc2lemOLD  37673  dvnprodlem3  37687  fourierdlem103  37937  fourierdlem104  37938  sge0iunmpt  38092  r19.32  38345  2rexrsb  38349  cbvral2  38350  2ralbiim  38352  rmoanim  38357  2rmoswap  38362  2reu3  38366  2reu4a  38367  ralnralall  38737  n0snor2el  38745  otiunsndisjX  38752  copisnmnd  39151  lindslinindsimp1  39594  lindslinindsimp2  39600  snlindsntor  39608  ldepslinc  39646  aacllem  39884
  Copyright terms: Public domain W3C validator