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

Theorem ralbii 2888
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 312 . 2  |-  ( ( x  e.  A  ->  ph )  <->  ( x  e.  A  ->  ps )
)
32ralbii2 2886 1  |-  ( A. x  e.  A  ph  <->  A. x  e.  A  ps )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1819   A.wral 2807
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632
This theorem depends on definitions:  df-bi 185  df-ral 2812
This theorem is referenced by:  2ralbii  2889  r3alOLD  2895  dfral2  2904  ralinexa  2909  rexanali  2910  nrexralim  2911  r19.23v  2937  r2exlem  2977  r19.26-2  2985  r19.26-3  2986  ralbiim  2989  r19.28v  2991  r19.30  3002  r19.32v  3003  r19.35  3004  cbvral2v  3092  cbvral3v  3094  sbralie  3097  ralcom4  3128  ralxpxfr2d  3224  reu8  3295  2reuswap  3302  2reu5lem2  3306  r19.12sn  4097  raldifsnb  4163  eqsn  4193  uni0b  4276  uni0c  4277  ssint  4304  iuniin  4343  iuneq2  4349  iunss  4373  ssiinf  4381  iinab  4393  iinun2  4398  iindif2  4401  iinin2  4402  iinuni  4419  sspwuni  4421  iinpw  4424  disjor  4441  disjxun  4454  dftr3  4554  trint  4565  reusv3  4664  reusv5OLD  4666  reuxfr2d  4679  otiunsndisj  4762  ssrel2  5102  reliun  5132  xpiindi  5148  rexiunxp  5153  ralxpf  5159  rexxpf  5160  dfse2  5380  asymref2  5394  rninxp  5453  dminxp  5454  cnviin  5550  cnvpo  5551  dffun9  5622  funcnv3  5655  fncnv  5658  fnres  5703  fnopabg  5710  mptfng  5712  fint  5770  funimass4  5924  fndmdifeq0  5994  funconstss  6006  f1ompt  6054  fconstfv  6134  idref  6154  dff13f  6168  dff14b  6179  weniso  6251  foov  6448  dfwe2  6616  tfis2f  6689  tfindes  6696  frxp  6909  tz7.48lem  7124  tz7.49  7128  oeordi  7254  ixpeq2  7502  ixpin  7513  ixpiin  7514  boxriin  7530  findcard3  7781  fimax2g  7784  fissuni  7843  indexfi  7846  dfsup2  7920  wemapsolem  7993  zfinf2  8076  oemapso  8118  zfregs2  8181  r1elss  8241  rankc1  8305  cp  8326  bnd2  8328  aceq1  8515  aceq2  8517  kmlem7  8553  kmlem12  8558  kmlem13  8559  kmlem15  8561  fin12  8810  ac6num  8876  ac6s2  8883  ac6sf  8886  ac6s4  8887  zorn2lem4  8896  zorn2lem6  8898  zorn2lem7  8899  zorng  8901  ttukeylem6  8911  brdom7disj  8926  brdom6disj  8927  fpwwe2  9038  fpwwe  9041  axgroth5  9219  axgroth4  9227  grothprim  9229  nqereu  9324  genpnnp  9400  dfinfmr  10540  infmsup  10541  infmrgelb  10543  infmrlb  10544  xrsupsslem  11523  xrinfmsslem  11524  xrinfmss2  11527  fzshftral  11791  fsuppmapnn0ub  12103  mptnn0fsuppr  12107  hashgt12el  12484  hashgt12el2  12485  hashbc  12505  rexfiuz  13191  clim0  13340  rpnnen2  13970  gcdcllem1  14160  vdwmc2  14508  vdwlem13  14522  vdwnn  14527  xpscf  14982  mreacs  15074  acsfn  15075  acsfn1  15077  acsfn2  15079  ispos2  15703  lublecllem  15744  oduglb  15895  odulub  15897  posglbd  15906  isnmnd  16050  gsumwspan  16140  isnsg2  16357  oppgid  16517  oppgcntz  16525  efgval2  16868  iscyggen2  17010  iscyg3  17015  oppr1  17409  isnirred  17475  lssne0  17723  isdomn2  18074  iunocv  18838  islindf4  18999  pmatcollpw2lem  19404  isbasis2g  19575  basdif0  19580  tgval2  19583  ntreq0  19704  isclo2  19715  opnnei  19747  neiptopnei  19759  lmres  19927  ist1-3  19976  cmpcov2  20016  cmpsub  20026  is1stc2  20068  1stccn  20089  kgencn  20182  eltx  20194  txkgen  20278  fbun  20466  trfbas  20470  fbunfip  20495  trfil2  20513  isufil2  20534  fixufil  20548  hausflim  20607  txflf  20632  fclsopn  20640  alexsubALTlem3  20674  iscau3  21842  iscau4  21843  caucfil  21847  bcth3  21895  ovolgelb  22016  dyadmax  22132  itg2leub  22266  itg2cn  22295  plydivex  22818  vieta1  22833  lgseisenlem2  23750  pnt3  23922  tglowdim2ln  24157  axcontlem12  24404  2spotiundisj  25188  frgrareg  25243  frgraregord013  25244  isgrpo2  25325  grpoidinvlem3  25334  nmoubi  25813  lnon0  25839  adjsym  26878  nmopub  26953  nmfnleub  26970  cvbr2  27328  chpssati  27408  chrelat2i  27410  chrelat3  27416  mdsymlem8  27455  ralcom4f  27501  moel  27508  uniinn0  27557  ssiun3  27562  disjnf  27570  disjorf  27577  disjunsn  27590  ac6sf2  27610  mptfnf  27642  nn0min  27763  tosglblem  27809  archiabl  27894  eulerpartlems  28474  eulerpartlemr  28488  eulerpartlemn  28495  ballotlem7  28649  subfacp1lem3  28801  cvmlift2lem1  28922  cvmlift2lem12  28934  untuni  29256  dfso3  29272  dfpo2  29359  setinds  29384  setinds2f  29385  elpotr  29387  dfon2lem7  29395  dfon2lem9  29397  wfis2fg  29465  frins2fg  29501  soseq  29508  dfint3  29764  brlb  29767  mblfinlem2  30214  ftc1anc  30260  gtinf  30299  filnetlem4  30361  inixp  30381  ac6gf  30385  heibor1lem  30467  heiborlem1  30469  iscrngo2  30557  ac6s3f  30741  n0el  30762  setindtrs  31129  undisjrab  31348  mccl  31767  ioodvbdlimc1lem2  31890  ioodvbdlimc2lem  31892  dvnprodlem3  31906  fourierdlem103  32153  fourierdlem104  32154  r19.32  32333  2rexrsb  32337  cbvral2  32338  2ralbiim  32340  rmoanim  32345  2rmoswap  32350  2reu3  32354  2reu4a  32355  ralnralall  32516  otiunsndisjX  32523  copisnmnd  32717  lindslinindsimp1  33160  lindslinindsimp2  33166  snlindsntor  33174  ldepslinc  33212  aacllem  33318  zfregs2VD  33742  bnj110  34017  bnj92  34021  bnj539  34050  bnj540  34051  bnj580  34072  bnj978  34108  bnj1047  34130  bnj1128  34147  bnj1417  34198  bnj1421  34199  bnj1312  34215  bnj1498  34218  lpssat  34839  lssat  34842  lcvbr2  34848  lcvbr3  34849  lfl1  34896  lub0N  35015  glb0N  35019  atlrelat1  35147  hlrelat2  35228  ispsubsp2  35571  pclclN  35716  cdleme25cv  36185  tendoeq2  36601  cdlemk35  36739  cllem0  37852  cotr2g  37887
  Copyright terms: Public domain W3C validator