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

Theorem ralbii 3119
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 325 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3117 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wcel 2140  wral 3051
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886
This theorem depends on definitions:  df-bi 197  df-ral 3056
This theorem is referenced by:  2ralbii  3120  dfral2  3133  ralinexa  3136  rexanali  3137  nrexralim  3138  r19.23v  3162  r19.26-2  3204  r19.26-3  3205  ralbiim  3208  r19.28v  3210  r19.30  3221  r19.32v  3222  r19.35  3223  ralcom13  3239  ralrot3  3241  cbvral2v  3319  cbvral3v  3321  sbralie  3324  ralcom4  3365  ralxpxfr2d  3467  reu8  3544  2reuswap  3552  2reu5lem2  3556  dfss5  4008  n0el  4084  ralnralall  4225  r19.12sn  4400  ssdifsnOLD  4465  raldifsnb  4472  eqsn  4507  eqsnOLD  4508  n0snor2el  4510  uni0b  4616  uni0c  4617  ssint  4646  iuniin  4684  iuneq2  4690  iunss  4714  ssiinf  4722  iinab  4734  iinun2  4739  iindif2  4742  iinin2  4743  iinuni  4762  sspwuni  4764  iinpw  4770  disjor  4787  disjxun  4803  dftr3  4909  trint  4921  reusv3  5026  reuxfr2d  5041  otiunsndisj  5131  ssrel2  5368  reliun  5396  xpiindi  5414  rexiunxp  5419  ralxpf  5425  rexxpf  5426  dfse2  5658  asymref2  5672  rninxp  5732  dminxp  5733  cnviin  5834  cnvpo  5835  wfis2fg  5879  dffun9  6079  funcnv3  6121  fncnv  6124  fnres  6169  mptfnf  6177  fnopabg  6179  mptfng  6181  fint  6246  funimass4  6411  fndmdifeq0  6488  funconstss  6500  f1ompt  6547  fconstfv  6642  idref  6664  dff13f  6678  dff14b  6693  weniso  6769  foov  6975  dfwe2  7148  tfis2f  7222  tfindes  7229  frxp  7457  tz7.48lem  7707  tz7.49  7711  oeordi  7839  ixpeq2  8091  ixpin  8102  ixpiin  8103  boxriin  8119  findcard3  8371  fimax2g  8374  fissuni  8439  indexfi  8442  dfsup2  8518  sup0riota  8539  infcllem  8561  wemapsolem  8623  zfinf2  8715  oemapso  8755  zfregs2  8785  r1elss  8845  rankc1  8909  cp  8930  bnd2  8932  aceq1  9151  aceq2  9153  kmlem7  9191  kmlem12  9196  kmlem13  9197  kmlem15  9199  fin12  9448  ac6num  9514  ac6s2  9521  ac6sf  9524  ac6s4  9525  zorn2lem4  9534  zorn2lem6  9536  zorn2lem7  9537  zorng  9539  ttukeylem6  9549  brdom7disj  9566  brdom6disj  9567  fpwwe2  9678  fpwwe  9681  axgroth5  9859  axgroth4  9867  grothprim  9869  nqereu  9964  genpnnp  10040  dfinfre  11217  infrenegsup  11219  xrsupsslem  12351  xrinfmsslem  12352  xrinfmss2  12355  fzshftral  12642  fsuppmapnn0ub  13010  mptnn0fsuppr  13014  hashgt12el  13423  hashgt12el2  13424  hashbc  13450  s3iunsndisj  13929  cotr2g  13937  rexfiuz  14307  clim0  14457  rpnnen2lem12  15174  gcdcllem1  15444  absproddvds  15553  coprmproddvdslem  15599  vdwmc2  15906  vdwlem13  15920  vdwnn  15925  xpscf  16449  mreacs  16541  acsfn  16542  acsfn1  16544  acsfn2  16546  ispos2  17170  lublecllem  17210  oduglb  17361  odulub  17363  posglbd  17372  isnmnd  17520  gsumwspan  17605  isnsg2  17846  oppgid  18007  oppgcntz  18015  efgval2  18358  iscyggen2  18504  iscyg3  18509  oppr1  18855  isnirred  18921  lssne0  19174  isdomn2  19522  iunocv  20248  islindf4  20400  pmatcollpw2lem  20805  isbasis2g  20975  basdif0  20980  tgval2  20983  ntreq0  21104  isclo2  21115  opnnei  21147  neiptopnei  21159  lmres  21327  ist1-3  21376  cmpcov2  21416  cmpsub  21426  is1stc2  21468  1stccn  21489  kgencn  21582  eltx  21594  txkgen  21678  fbun  21866  trfbas  21870  fbunfip  21895  trfil2  21913  isufil2  21934  fixufil  21948  hausflim  22007  txflf  22032  fclsopn  22040  alexsubALTlem3  22075  isclmp  23118  iscau3  23297  iscau4  23298  caucfil  23302  bcth3  23349  ovolgelb  23469  dyadmax  23587  itg2leub  23721  itg2cn  23750  plydivex  24272  vieta1  24287  lgseisenlem2  25322  pnt3  25522  tglowdim2ln  25767  axcontlem12  26076  numedglnl  26260  vtxd0nedgb  26616  wlkvtxedg  26772  pthd  26897  2pthdlem1  27072  clwlkclwwlk  27147  clwlksfclwwlkOLD  27238  3pthdlem1  27338  frgrregord013  27585  grpoidinvlem3  27691  nmoubi  27958  lnon0  27984  adjsym  29023  nmopub  29098  nmfnleub  29115  cvbr2  29473  chpssati  29553  chrelat2i  29555  chrelat3  29561  mdsymlem8  29600  ralcom4f  29647  moel  29654  uniinn0  29695  ssiun3  29705  disjnf  29713  disjorf  29721  disjunsn  29736  ac6sf2  29760  nn0min  29898  tosglblem  30000  archiabl  30083  eulerpartlems  30753  eulerpartlemr  30767  eulerpartlemn  30774  ballotlem7  30928  bnj110  31257  bnj92  31261  bnj539  31290  bnj540  31291  bnj580  31312  bnj978  31348  bnj1047  31370  bnj1128  31387  bnj1417  31438  bnj1421  31439  bnj1312  31455  bnj1498  31458  subfacp1lem3  31493  cvmlift2lem1  31613  cvmlift2lem12  31625  untuni  31915  dfso3  31930  dfpo2  31974  elintfv  31991  setinds  32010  setinds2f  32011  elpotr  32013  dfon2lem7  32021  dfon2lem9  32023  frins2fg  32075  soseq  32082  nosepon  32146  nomaxmo  32175  nosupbnd1lem4  32185  conway  32238  ssltun2  32244  etasslt  32248  slerec  32251  dfint3  32387  brlb  32390  gtinfOLD  32642  filnetlem4  32704  phpreu  33725  ptrecube  33741  poimirlem1  33742  poimirlem25  33766  poimirlem26  33767  poimirlem27  33768  poimirlem30  33771  mblfinlem2  33779  ftc1anc  33825  inixp  33855  ac6gf  33859  heibor1lem  33940  heiborlem1  33942  iscrngo2  34128  ac6s3f  34311  3ralbii  34357  idinxpssinxp2  34432  n0elqs  34441  ineleq  34461  refrelcosslem  34554  refrelcoss3  34555  lpssat  34822  lssat  34825  lcvbr2  34831  lcvbr3  34832  lfl1  34879  lub0N  34998  glb0N  35002  atlrelat1  35130  hlrelat2  35211  ispsubsp2  35554  pclclN  35699  cdleme25cv  36167  tendoeq2  36583  cdlemk35  36721  setindtrs  38113  cllem0  38392  ss2iundf  38472  ntrneixb  38914  gneispace  38953  undisjrab  39026  zfregs2VD  39594  iunssf  39781  disjinfi  39898  iuneqfzuz  40068  mccl  40352  limsupub  40458  limsuppnflem  40464  limsupre2lem  40478  lmbr3v  40499  ioodvbdlimc1lem2  40669  ioodvbdlimc2lem  40671  dvnprodlem3  40685  fourierdlem103  40948  fourierdlem104  40949  sge0iunmpt  41157  meaiuninc3v  41223  hoidmvle  41339  issmff  41468  r19.32  41692  2rexrsb  41696  cbvral2  41697  2ralbiim  41699  rmoanim  41704  2rmoswap  41709  2reu3  41713  2reu4a  41714  otiunsndisjX  41825  copisnmnd  42338  lindslinindsimp1  42775  lindslinindsimp2  42781  snlindsntor  42789  ldepslinc  42827  setrec1lem3  42965  aacllem  43079
  Copyright terms: Public domain W3C validator