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

Theorem ralbii 2832
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 310 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2830 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1840   A.wral 2751
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650
This theorem depends on definitions:  df-bi 185  df-ral 2756
This theorem is referenced by:  2ralbii  2833  r3alOLD  2839  dfral2  2848  ralinexa  2853  rexanali  2854  nrexralim  2855  r19.23v  2881  r2exlem  2924  r19.26-2  2932  r19.26-3  2933  ralbiim  2936  r19.28v  2938  r19.30  2949  r19.32v  2950  r19.35  2951  cbvral2v  3039  cbvral3v  3041  sbralie  3044  ralcom4  3075  ralxpxfr2d  3171  reu8  3242  2reuswap  3249  2reu5lem2  3253  r19.12sn  4034  raldifsnb  4100  eqsn  4130  uni0b  4213  uni0c  4214  ssint  4240  iuniin  4279  iuneq2  4285  iunss  4309  ssiinf  4317  iinab  4329  iinun2  4334  iindif2  4337  iinin2  4338  iinuni  4355  sspwuni  4357  iinpw  4360  disjor  4377  disjxun  4390  dftr3  4490  trint  4501  reusv3  4599  reuxfr2d  4611  otiunsndisj  4693  ssrel2  5033  reliun  5062  xpiindi  5078  rexiunxp  5083  ralxpf  5089  rexxpf  5090  dfse2  5309  asymref2  5324  rninxp  5383  dminxp  5384  cnviin  5480  cnvpo  5481  dffun9  5551  funcnv3  5584  fncnv  5587  fnres  5632  mptfnf  5639  fnopabg  5641  mptfng  5643  fint  5701  funimass4  5854  fndmdifeq0  5925  funconstss  5937  f1ompt  5985  fconstfv  6068  idref  6088  dff13f  6102  dff14b  6113  weniso  6187  foov  6384  dfwe2  6553  tfis2f  6626  tfindes  6633  frxp  6846  tz7.48lem  7061  tz7.49  7065  oeordi  7191  ixpeq2  7439  ixpin  7450  ixpiin  7451  boxriin  7467  findcard3  7715  fimax2g  7718  fissuni  7777  indexfi  7780  dfsup2  7854  wemapsolem  7927  zfinf2  8010  oemapso  8051  zfregs2  8114  r1elss  8174  rankc1  8238  cp  8259  bnd2  8261  aceq1  8448  aceq2  8450  kmlem7  8486  kmlem12  8491  kmlem13  8492  kmlem15  8494  fin12  8743  ac6num  8809  ac6s2  8816  ac6sf  8819  ac6s4  8820  zorn2lem4  8829  zorn2lem6  8831  zorn2lem7  8832  zorng  8834  ttukeylem6  8844  brdom7disj  8859  brdom6disj  8860  fpwwe2  8969  fpwwe  8972  axgroth5  9150  axgroth4  9158  grothprim  9160  nqereu  9255  genpnnp  9331  dfinfmr  10478  infmsup  10479  infmrgelb  10481  infmrlb  10482  xrsupsslem  11467  xrinfmsslem  11468  xrinfmss2  11471  fzshftral  11736  fsuppmapnn0ub  12053  mptnn0fsuppr  12057  hashgt12el  12435  hashgt12el2  12436  hashbc  12456  cotr2g  12864  rexfiuz  13234  clim0  13383  rpnnen2  14058  gcdcllem1  14248  vdwmc2  14596  vdwlem13  14610  vdwnn  14615  xpscf  15070  mreacs  15162  acsfn  15163  acsfn1  15165  acsfn2  15167  ispos2  15791  lublecllem  15832  oduglb  15983  odulub  15985  posglbd  15994  isnmnd  16138  gsumwspan  16228  isnsg2  16445  oppgid  16605  oppgcntz  16613  efgval2  16956  iscyggen2  17098  iscyg3  17103  oppr1  17493  isnirred  17559  lssne0  17807  isdomn2  18158  iunocv  18900  islindf4  19055  pmatcollpw2lem  19460  isbasis2g  19631  basdif0  19636  tgval2  19639  ntreq0  19761  isclo2  19772  opnnei  19804  neiptopnei  19816  lmres  19984  ist1-3  20033  cmpcov2  20073  cmpsub  20083  is1stc2  20125  1stccn  20146  kgencn  20239  eltx  20251  txkgen  20335  fbun  20523  trfbas  20527  fbunfip  20552  trfil2  20570  isufil2  20591  fixufil  20605  hausflim  20664  txflf  20689  fclsopn  20697  alexsubALTlem3  20731  iscau3  21899  iscau4  21900  caucfil  21904  bcth3  21952  ovolgelb  22073  dyadmax  22189  itg2leub  22323  itg2cn  22352  plydivex  22875  vieta1  22890  lgseisenlem2  23896  pnt3  24068  tglowdim2ln  24312  axcontlem12  24577  2spotiundisj  25361  frgrareg  25416  frgraregord013  25417  isgrpo2  25494  grpoidinvlem3  25503  nmoubi  25982  lnon0  26008  adjsym  27046  nmopub  27121  nmfnleub  27138  cvbr2  27496  chpssati  27576  chrelat2i  27578  chrelat3  27584  mdsymlem8  27623  ralcom4f  27669  moel  27678  uniinn0  27726  ssiun3  27736  disjnf  27744  disjorf  27752  disjunsn  27767  ac6sf2  27790  nn0min  27944  tosglblem  27990  archiabl  28075  eulerpartlems  28686  eulerpartlemr  28700  eulerpartlemn  28707  ballotlem7  28861  bnj110  29119  bnj92  29123  bnj539  29152  bnj540  29153  bnj580  29174  bnj978  29210  bnj1047  29232  bnj1128  29249  bnj1417  29300  bnj1421  29301  bnj1312  29317  bnj1498  29320  subfacp1lem3  29355  cvmlift2lem1  29475  cvmlift2lem12  29487  untuni  29786  dfso3  29802  dfpo2  29849  setinds  29878  setinds2f  29879  elpotr  29881  dfon2lem7  29889  dfon2lem9  29891  wfis2fg  29959  frins2fg  29995  soseq  30002  dfint3  30258  brlb  30261  gtinf  30530  filnetlem4  30592  mblfinlem2  31388  ftc1anc  31435  inixp  31465  ac6gf  31469  heibor1lem  31551  heiborlem1  31553  iscrngo2  31641  ac6s3f  31825  n0el  31846  lpssat  31995  lssat  31998  lcvbr2  32004  lcvbr3  32005  lfl1  32052  lub0N  32171  glb0N  32175  atlrelat1  32303  hlrelat2  32384  ispsubsp2  32727  pclclN  32872  cdleme25cv  33341  tendoeq2  33757  cdlemk35  33895  setindtrs  35293  cllem0  35581  ss2iundf  35602  undisjrab  35998  zfregs2VD  36635  mccl  36941  ioodvbdlimc1lem2  37064  ioodvbdlimc2lem  37066  dvnprodlem3  37080  fourierdlem103  37327  fourierdlem104  37328  r19.32  37507  2rexrsb  37511  cbvral2  37512  2ralbiim  37514  rmoanim  37519  2rmoswap  37524  2reu3  37528  2reu4a  37529  ralnralall  37859  otiunsndisjX  37866  copisnmnd  38059  lindslinindsimp1  38502  lindslinindsimp2  38508  snlindsntor  38516  ldepslinc  38554  aacllem  38794
  Copyright terms: Public domain W3C validator