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

Theorem ralbii 2976
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 (𝜑𝜓)
Assertion
Ref Expression
ralbii (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)

Proof of Theorem ralbii
StepHypRef Expression
1 ralbii.1 . . 3 (𝜑𝜓)
21imbi2i 326 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 2974 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 1987  wral 2908
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734
This theorem depends on definitions:  df-bi 197  df-ral 2913
This theorem is referenced by:  2ralbii  2977  dfral2  2990  ralinexa  2993  rexanali  2994  nrexralim  2995  r19.23v  3018  r19.26-2  3060  r19.26-3  3061  ralbiim  3064  r19.28v  3066  r19.30  3076  r19.32v  3077  r19.35  3078  ralcom13  3094  ralrot3  3096  cbvral2v  3171  cbvral3v  3173  sbralie  3176  ralcom4  3214  ralxpxfr2d  3316  reu8  3389  2reuswap  3397  2reu5lem2  3401  dfss5  3846  ralnralall  4058  r19.12sn  4232  raldifsnb  4301  eqsn  4336  eqsnOLD  4337  n0snor2el  4339  uni0b  4436  uni0c  4437  ssint  4465  iuniin  4504  iuneq2  4510  iunss  4534  ssiinf  4542  iinab  4554  iinun2  4559  iindif2  4562  iinin2  4563  iinuni  4582  sspwuni  4584  iinpw  4590  disjor  4607  disjxun  4621  dftr3  4726  trint  4738  reusv3  4846  reuxfr2d  4861  otiunsndisj  4950  ssrel2  5181  reliun  5210  xpiindi  5227  rexiunxp  5232  ralxpf  5238  rexxpf  5239  dfse2  5468  asymref2  5482  rninxp  5542  dminxp  5543  cnviin  5641  cnvpo  5642  wfis2fg  5686  dffun9  5886  funcnv3  5927  fncnv  5930  fnres  5975  mptfnf  5982  fnopabg  5984  mptfng  5986  fint  6051  funimass4  6214  fndmdifeq0  6289  funconstss  6301  f1ompt  6348  fconstfv  6441  idref  6464  dff13f  6478  dff14b  6493  weniso  6569  foov  6773  dfwe2  6943  tfis2f  7017  tfindes  7024  frxp  7247  tz7.48lem  7496  tz7.49  7500  oeordi  7627  ixpeq2  7882  ixpin  7893  ixpiin  7894  boxriin  7910  findcard3  8163  fimax2g  8166  fissuni  8231  indexfi  8234  dfsup2  8310  sup0riota  8331  infcllem  8353  wemapsolem  8415  zfinf2  8499  oemapso  8539  zfregs2  8569  r1elss  8629  rankc1  8693  cp  8714  bnd2  8716  aceq1  8900  aceq2  8902  kmlem7  8938  kmlem12  8943  kmlem13  8944  kmlem15  8946  fin12  9195  ac6num  9261  ac6s2  9268  ac6sf  9271  ac6s4  9272  zorn2lem4  9281  zorn2lem6  9283  zorn2lem7  9284  zorng  9286  ttukeylem6  9296  brdom7disj  9313  brdom6disj  9314  fpwwe2  9425  fpwwe  9428  axgroth5  9606  axgroth4  9614  grothprim  9616  nqereu  9711  genpnnp  9787  dfinfre  10964  infrenegsup  10966  xrsupsslem  12096  xrinfmsslem  12097  xrinfmss2  12100  fzshftral  12385  fsuppmapnn0ub  12751  mptnn0fsuppr  12755  hashgt12el  13166  hashgt12el2  13167  hashbc  13191  s3iunsndisj  13657  cotr2g  13665  rexfiuz  14037  clim0  14187  rpnnen2lem12  14898  gcdcllem1  15164  absproddvds  15273  coprmproddvdslem  15319  vdwmc2  15626  vdwlem13  15640  vdwnn  15645  xpscf  16166  mreacs  16259  acsfn  16260  acsfn1  16262  acsfn2  16264  ispos2  16888  lublecllem  16928  oduglb  17079  odulub  17081  posglbd  17090  isnmnd  17238  gsumwspan  17323  isnsg2  17564  oppgid  17726  oppgcntz  17734  efgval2  18077  iscyggen2  18223  iscyg3  18228  oppr1  18574  isnirred  18640  lssne0  18891  isdomn2  19239  iunocv  19965  islindf4  20117  pmatcollpw2lem  20522  isbasis2g  20692  basdif0  20697  tgval2  20700  ntreq0  20821  isclo2  20832  opnnei  20864  neiptopnei  20876  lmres  21044  ist1-3  21093  cmpcov2  21133  cmpsub  21143  is1stc2  21185  1stccn  21206  kgencn  21299  eltx  21311  txkgen  21395  fbun  21584  trfbas  21588  fbunfip  21613  trfil2  21631  isufil2  21652  fixufil  21666  hausflim  21725  txflf  21750  fclsopn  21758  alexsubALTlem3  21793  isclmp  22837  iscau3  23016  iscau4  23017  caucfil  23021  bcth3  23068  ovolgelb  23188  dyadmax  23306  itg2leub  23441  itg2cn  23470  plydivex  23990  vieta1  24005  lgseisenlem2  25035  pnt3  25235  tglowdim2ln  25480  axcontlem12  25789  vtxd0nedgb  26304  pthd  26568  2pthdlem1  26729  2wspiundisj  26758  3pthdlem1  26924  frgrregord013  27141  grpoidinvlem3  27248  nmoubi  27515  lnon0  27541  adjsym  28580  nmopub  28655  nmfnleub  28672  cvbr2  29030  chpssati  29110  chrelat2i  29112  chrelat3  29118  mdsymlem8  29157  ralcom4f  29204  moel  29212  uniinn0  29253  ssiun3  29263  disjnf  29270  disjorf  29278  disjunsn  29293  ac6sf2  29313  nn0min  29450  tosglblem  29496  archiabl  29579  eulerpartlems  30245  eulerpartlemr  30259  eulerpartlemn  30266  ballotlem7  30420  bnj110  30689  bnj92  30693  bnj539  30722  bnj540  30723  bnj580  30744  bnj978  30780  bnj1047  30802  bnj1128  30819  bnj1417  30870  bnj1421  30871  bnj1312  30887  bnj1498  30890  subfacp1lem3  30925  cvmlift2lem1  31045  cvmlift2lem12  31057  untuni  31347  dfso3  31363  dfpo2  31406  setinds  31437  setinds2f  31438  elpotr  31440  dfon2lem7  31448  dfon2lem9  31450  frins2fg  31498  soseq  31505  nosepon  31576  noprefixmo  31626  dfint3  31754  brlb  31757  gtinfOLD  32009  filnetlem4  32071  phpreu  33064  ptrecube  33080  poimirlem1  33081  poimirlem25  33105  poimirlem26  33106  poimirlem27  33107  poimirlem30  33110  mblfinlem2  33118  ftc1anc  33164  inixp  33194  ac6gf  33198  heibor1lem  33279  heiborlem1  33281  iscrngo2  33467  ac6s3f  33650  n0el  33665  lpssat  33819  lssat  33822  lcvbr2  33828  lcvbr3  33829  lfl1  33876  lub0N  33995  glb0N  33999  atlrelat1  34127  hlrelat2  34208  ispsubsp2  34551  pclclN  34696  cdleme25cv  35165  tendoeq2  35581  cdlemk35  35719  setindtrs  37111  cllem0  37391  ss2iundf  37471  ntrneixb  37914  gneispace  37953  undisjrab  38026  zfregs2VD  38598  iunssf  38785  disjinfi  38889  iuneqfzuz  39050  mccl  39266  limsupub  39372  limsuppnflem  39378  limsupre2lem  39392  ioodvbdlimc1lem2  39484  ioodvbdlimc2lem  39486  dvnprodlem3  39500  fourierdlem103  39763  fourierdlem104  39764  sge0iunmpt  39972  hoidmvle  40151  issmff  40280  r19.32  40501  2rexrsb  40505  cbvral2  40506  2ralbiim  40508  rmoanim  40513  2rmoswap  40518  2reu3  40522  2reu4a  40523  otiunsndisjX  40625  copisnmnd  41127  lindslinindsimp1  41564  lindslinindsimp2  41570  snlindsntor  41578  ldepslinc  41616  ssdifsn  41752  setrec1lem3  41759  aacllem  41880
  Copyright terms: Public domain W3C validator