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

Theorem ralbii 2963
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 2961 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wb 195  wcel 1977  wral 2896
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728
This theorem depends on definitions:  df-bi 196  df-ral 2901
This theorem is referenced by:  2ralbii  2964  dfral2  2977  ralinexa  2980  rexanali  2981  nrexralim  2982  r19.23v  3005  r19.26-2  3047  r19.26-3  3048  ralbiim  3051  r19.28v  3053  r19.30  3063  r19.32v  3064  r19.35  3065  cbvral2v  3155  cbvral3v  3157  sbralie  3160  ralcom4  3197  ralxpxfr2d  3298  reu8  3369  2reuswap  3377  2reu5lem2  3381  r19.12sn  4199  raldifsnb  4266  eqsn  4301  eqsnOLD  4302  n0snor2el  4304  uni0b  4399  uni0c  4400  ssint  4428  iuniin  4467  iuneq2  4473  iunss  4497  ssiinf  4505  iinab  4517  iinun2  4522  iindif2  4525  iinin2  4526  iinuni  4545  sspwuni  4547  iinpw  4550  disjor  4567  disjxun  4581  dftr3  4684  trint  4696  reusv3  4802  reuxfr2d  4817  otiunsndisj  4905  ssrel2  5133  reliun  5162  xpiindi  5179  rexiunxp  5184  ralxpf  5190  rexxpf  5191  dfse2  5418  asymref2  5432  rninxp  5492  dminxp  5493  cnviin  5589  cnvpo  5590  wfis2fg  5634  dffun9  5832  funcnv3  5873  fncnv  5876  fnres  5921  mptfnf  5928  fnopabg  5930  mptfng  5932  fint  5997  funimass4  6157  fndmdifeq0  6231  funconstss  6243  f1ompt  6290  fconstfv  6381  idref  6403  dff13f  6417  dff14b  6428  weniso  6504  foov  6706  dfwe2  6873  tfis2f  6947  tfindes  6954  frxp  7174  tz7.48lem  7423  tz7.49  7427  oeordi  7554  ixpeq2  7808  ixpin  7819  ixpiin  7820  boxriin  7836  findcard3  8088  fimax2g  8091  fissuni  8154  indexfi  8157  dfsup2  8233  sup0riota  8254  infcllem  8276  wemapsolem  8338  zfinf2  8422  oemapso  8462  zfregs2  8492  r1elss  8552  rankc1  8616  cp  8637  bnd2  8639  aceq1  8823  aceq2  8825  kmlem7  8861  kmlem12  8866  kmlem13  8867  kmlem15  8869  fin12  9118  ac6num  9184  ac6s2  9191  ac6sf  9194  ac6s4  9195  zorn2lem4  9204  zorn2lem6  9206  zorn2lem7  9207  zorng  9209  ttukeylem6  9219  brdom7disj  9234  brdom6disj  9235  fpwwe2  9344  fpwwe  9347  axgroth5  9525  axgroth4  9533  grothprim  9535  nqereu  9630  genpnnp  9706  dfinfre  10881  infrenegsup  10883  xrsupsslem  12009  xrinfmsslem  12010  xrinfmss2  12013  fzshftral  12297  fsuppmapnn0ub  12657  mptnn0fsuppr  12661  hashgt12el  13070  hashgt12el2  13071  hashbc  13094  s3iunsndisj  13555  cotr2g  13563  rexfiuz  13935  clim0  14085  rpnnen2lem12  14793  gcdcllem1  15059  absproddvds  15168  coprmproddvdslem  15214  vdwmc2  15521  vdwlem13  15535  vdwnn  15540  xpscf  16049  mreacs  16142  acsfn  16143  acsfn1  16145  acsfn2  16147  ispos2  16771  lublecllem  16811  oduglb  16962  odulub  16964  posglbd  16973  isnmnd  17121  gsumwspan  17206  isnsg2  17447  oppgid  17609  oppgcntz  17617  efgval2  17960  iscyggen2  18106  iscyg3  18111  oppr1  18457  isnirred  18523  lssne0  18772  isdomn2  19120  iunocv  19844  islindf4  19996  pmatcollpw2lem  20401  isbasis2g  20563  basdif0  20568  tgval2  20571  ntreq0  20691  isclo2  20702  opnnei  20734  neiptopnei  20746  lmres  20914  ist1-3  20963  cmpcov2  21003  cmpsub  21013  is1stc2  21055  1stccn  21076  kgencn  21169  eltx  21181  txkgen  21265  fbun  21454  trfbas  21458  fbunfip  21483  trfil2  21501  isufil2  21522  fixufil  21536  hausflim  21595  txflf  21620  fclsopn  21628  alexsubALTlem3  21663  isclmp  22705  iscau3  22884  iscau4  22885  caucfil  22889  bcth3  22936  ovolgelb  23055  dyadmax  23172  itg2leub  23307  itg2cn  23336  plydivex  23856  vieta1  23871  lgseisenlem2  24901  pnt3  25101  tglowdim2ln  25346  axcontlem12  25655  2spotiundisj  26589  frgrareg  26644  frgraregord013  26645  grpoidinvlem3  26744  nmoubi  27011  lnon0  27037  adjsym  28076  nmopub  28151  nmfnleub  28168  cvbr2  28526  chpssati  28606  chrelat2i  28608  chrelat3  28614  mdsymlem8  28653  ralcom4f  28700  moel  28707  uniinn0  28749  ssiun3  28759  disjnf  28766  disjorf  28774  disjunsn  28789  ac6sf2  28810  nn0min  28954  tosglblem  29000  archiabl  29083  eulerpartlems  29749  eulerpartlemr  29763  eulerpartlemn  29770  ballotlem7  29924  bnj110  30182  bnj92  30186  bnj539  30215  bnj540  30216  bnj580  30237  bnj978  30273  bnj1047  30295  bnj1128  30312  bnj1417  30363  bnj1421  30364  bnj1312  30380  bnj1498  30383  subfacp1lem3  30418  cvmlift2lem1  30538  cvmlift2lem12  30550  untuni  30840  dfso3  30856  dfpo2  30898  setinds  30927  setinds2f  30928  elpotr  30930  dfon2lem7  30938  dfon2lem9  30940  frins2fg  30988  soseq  30995  nosepon  31066  dfint3  31229  brlb  31232  gtinfOLD  31484  filnetlem4  31546  phpreu  32563  ptrecube  32579  poimirlem1  32580  poimirlem25  32604  poimirlem26  32605  poimirlem27  32606  poimirlem30  32609  mblfinlem2  32617  ftc1anc  32663  inixp  32693  ac6gf  32697  heibor1lem  32778  heiborlem1  32780  iscrngo2  32966  ac6s3f  33149  n0el  33164  lpssat  33318  lssat  33321  lcvbr2  33327  lcvbr3  33328  lfl1  33375  lub0N  33494  glb0N  33498  atlrelat1  33626  hlrelat2  33707  ispsubsp2  34050  pclclN  34195  cdleme25cv  34664  tendoeq2  35080  cdlemk35  35218  setindtrs  36610  cllem0  36890  ss2iundf  36970  ntrneixb  37413  gneispace  37452  undisjrab  37527  zfregs2VD  38098  iunssf  38290  disjinfi  38375  iuneqfzuz  38492  mccl  38665  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  dvnprodlem3  38838  fourierdlem103  39102  fourierdlem104  39103  sge0iunmpt  39311  hoidmvle  39490  issmff  39620  r19.32  39816  2rexrsb  39820  cbvral2  39821  2ralbiim  39823  rmoanim  39828  2rmoswap  39833  2reu3  39837  2reu4a  39838  dfss7  40304  ralnralall  40307  otiunsndisjX  40317  vtxd0nedgb  40703  pthd  40975  2pthdlem1  41137  2wspiundisj  41166  3pthdlem1  41331  av-frgraregord013  41549  copisnmnd  41599  lindslinindsimp1  42040  lindslinindsimp2  42046  snlindsntor  42054  ldepslinc  42092  ssdifsn  42228  setrec1lem3  42235  aacllem  42356
  Copyright terms: Public domain W3C validator