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

Theorem ralbii 3160
 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 339 . 2 ((𝑥𝐴𝜑) ↔ (𝑥𝐴𝜓))
32ralbii2 3158 1 (∀𝑥𝐴 𝜑 ↔ ∀𝑥𝐴 𝜓)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∈ wcel 2115  ∀wral 3133 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811 This theorem depends on definitions:  df-bi 210  df-ral 3138 This theorem is referenced by:  2ralbii  3161  r19.26-2  3166  r19.26-3  3167  ralbiim  3169  r19.28vOLD  3182  dfral2  3231  ralnex2  3254  ralinexa  3256  rexanali  3257  nrexralim  3258  nelb  3260  r19.23v  3271  r19.30OLD  3330  r19.32v  3331  ralcom13  3350  ralrot3  3352  cbvral2vw  3446  cbvral3vw  3448  cbvral2v  3449  cbvral3v  3451  sbralie  3456  ralcom4OLD  3511  ralxpxfr2d  3625  reu8  3710  2reuswap  3723  2reu5lem2  3733  2rmoswap  3738  rmoanim  3861  rmoanimALT  3862  dfss5  4226  n0el  4304  ralnralall  4441  2reu4lem  4448  r19.12sn  4641  raldifsnb  4713  eqsn  4746  n0snor2el  4748  uni0b  4850  uni0c  4851  ssint  4878  iuniin  4917  iuneq2  4924  iunss  4955  ssiinf  4964  iinab  4976  iinun2  4981  iindif1  4983  iindif2  4985  iinin2  4986  iinuni  5006  sspwuni  5008  iinpw  5014  disjor  5032  disjxun  5050  dftr3  5162  reusv3  5293  otiunsndisj  5397  ssrel2  5646  reliun  5676  xpiindi  5693  rexiunxp  5698  ralxpf  5704  rexxpf  5705  dfse2  5950  idrefALT  5960  asymref2  5964  rninxp  6023  dminxp  6024  cnviin  6124  cnvpo  6125  wfis2fg  6172  dffun9  6372  funcnv3  6412  fncnv  6415  fnres  6463  mptfnf  6472  fnopabg  6474  mptfng  6476  fint  6548  funimass4  6721  fndmdifeq0  6805  funconstss  6817  f1ompt  6866  idref  6899  fconstfv  6966  dff13f  7006  dff14b  7021  weniso  7100  foov  7316  dfwe2  7490  tfis2f  7564  tfindes  7571  frxp  7816  tz7.48lem  8073  tz7.49  8077  oeordi  8209  ixpeq2  8471  ixpin  8483  ixpiin  8484  boxriin  8500  findcard3  8758  fimax2g  8761  fissuni  8826  indexfi  8829  dfsup2  8905  sup0riota  8926  infcllem  8948  wemapsolem  9011  zfinf2  9102  oemapso  9142  zfregs2  9172  r1elss  9232  rankc1  9296  cp  9317  bnd2  9319  aceq1  9541  aceq2  9543  kmlem7  9580  kmlem12  9585  kmlem13  9586  kmlem15  9588  fin12  9833  ac6num  9899  ac6s2  9906  ac6sf  9909  ac6s4  9910  zorn2lem4  9919  zorn2lem6  9921  zorn2lem7  9922  zorng  9924  ttukeylem6  9934  brdom7disj  9951  brdom6disj  9952  fpwwe2  10063  fpwwe  10066  axgroth5  10244  axgroth4  10252  grothprim  10254  nqereu  10349  dfinfre  11618  infrenegsup  11620  xrsupsslem  12697  xrinfmsslem  12698  xrinfmss2  12701  fzshftral  12999  fsuppmapnn0ub  13367  mptnn0fsuppr  13371  hashgt12el  13788  hashgt12el2  13789  hashbc  13816  s3iunsndisj  14328  cotr2g  14336  rexfiuz  14707  clim0  14863  rpnnen2lem12  15578  gcdcllem1  15846  absproddvds  15959  coprmproddvdslem  16004  vdwmc2  16313  vdwlem13  16327  vdwnn  16332  xpscf  16838  mreacs  16929  acsfn  16930  acsfn1  16932  acsfn2  16934  ispos2  17558  lublecllem  17598  oduglb  17749  odulub  17751  posglbd  17760  isnmnd  17915  gsumwspan  18011  smndex2dnrinv  18080  isnsg2  18308  oppgid  18484  oppgcntz  18492  efgval2  18850  iscyggen2  19000  iscyg3  19005  oppr1  19387  isnirred  19453  lssne0  19722  isdomn2  20072  iunocv  20377  islindf4  20534  pmatcollpw2lem  21388  isbasis2g  21559  basdif0  21564  tgval2  21567  ntreq0  21688  isclo2  21699  opnnei  21731  neiptopnei  21743  lmres  21911  ist1-3  21960  cmpcov2  22001  cmpsub  22011  is1stc2  22053  1stccn  22074  kgencn  22167  eltx  22179  txkgen  22263  fbun  22451  trfbas  22455  fbunfip  22480  trfil2  22498  isufil2  22519  fixufil  22533  hausflim  22592  txflf  22617  fclsopn  22625  alexsubALTlem3  22660  isclmp  23708  iscau3  23888  iscau4  23889  caucfil  23893  bcth3  23941  ovolgelb  24090  dyadmax  24208  itg2leub  24344  itg2cn  24373  plydivex  24899  vieta1  24914  lgseisenlem2  25966  pnt3  26202  tglowdim2ln  26451  axcontlem12  26775  elntg2  26785  numedglnl  26943  vtxd0nedgb  27284  wlkvtxedg  27439  pthd  27564  2pthdlem1  27722  clwlkclwwlk  27793  3pthdlem1  27955  frgrregord013  28186  grpoidinvlem3  28295  nmoubi  28561  lnon0  28587  adjsym  29622  nmopub  29697  nmfnleub  29714  cvbr2  30072  chpssati  30152  chrelat2i  30154  chrelat3  30160  mdsymlem8  30199  nelbOLD  30244  ralcom4f  30245  moel  30264  reuxfrdf  30267  uniinn0  30316  ssiun3  30324  disjnf  30334  disjorf  30343  disjunsn  30358  ac6sf2  30384  nn0min  30550  tosglblem  30670  archiabl  30862  eulerpartlems  31678  eulerpartlemr  31692  eulerpartlemn  31699  ballotlem7  31853  bnj110  32190  bnj92  32194  bnj539  32223  bnj540  32224  bnj580  32245  bnj978  32281  bnj1047  32305  bnj1128  32322  bnj1417  32373  bnj1421  32374  bnj1312  32390  bnj1498  32393  lfuhgr3  32426  subfacp1lem3  32489  cvmlift2lem1  32609  cvmlift2lem12  32621  satfv1  32670  fmlaomn0  32697  fmla0disjsuc  32705  fmlasucdisj  32706  untuni  32995  dfso3  33010  dfpo2  33051  elintfv  33067  setinds  33083  setinds2f  33084  elpotr  33086  dfon2lem7  33094  dfon2lem9  33096  frpoins2fg  33142  frins2fg  33149  soseq  33156  nosepon  33232  nomaxmo  33261  nosupbnd1lem4  33271  conway  33324  ssltun2  33330  etasslt  33334  slerec  33337  dfint3  33473  brlb  33476  filnetlem4  33789  bj-reabeq  34410  ctbssinf  34771  fvineqsneq  34777  pibt2  34782  phpreu  34989  ptrecube  35005  poimirlem1  35006  poimirlem25  35030  poimirlem26  35031  poimirlem27  35032  poimirlem30  35035  mblfinlem2  35043  ftc1anc  35086  inixp  35114  ac6gf  35118  heibor1lem  35195  heiborlem1  35197  iscrngo2  35383  ac6s3f  35557  3ralbii  35618  idinxpssinxp2  35683  n0elqs  35691  ineleq  35716  refrelcosslem  35810  refrelcoss3  35811  lpssat  36257  lssat  36260  lcvbr2  36266  lcvbr3  36267  lfl1  36314  lub0N  36433  glb0N  36437  atlrelat1  36565  hlrelat2  36647  ispsubsp2  36990  pclclN  37135  cdleme25cv  37602  tendoeq2  38018  cdlemk35  38156  setindtrs  39886  cllem0  40185  ss2iundf  40280  ntrneixb  40721  gneispace  40760  expandral  40922  ismnuprim  40926  undisjrab  40934  zfregs2VD  41471  iunssf  41648  disjinfi  41749  iuneqfzuz  41897  mccl  42170  limsupub  42276  limsuppnflem  42282  limsupre2lem  42296  lmbr3v  42317  liminfpnfuz  42388  xlimpnfxnegmnf2  42430  ioodvbdlimc1lem2  42504  ioodvbdlimc2lem  42506  dvnprodlem3  42520  fourierdlem103  42781  fourierdlem104  42782  sge0iunmpt  42987  meaiuninc3v  43053  hoidmvle  43169  issmff  43298  r19.32  43583  2rexrsb  43587  cbvral2  43588  2ralbiim  43590  2reu3  43596  2reu8i  43599  otiunsndisjX  43765  0nelsetpreimafv  43837  copisnmnd  44359  lindslinindsimp1  44796  lindslinindsimp2  44802  snlindsntor  44810  ldepslinc  44848  setrec1lem3  45149  aacllem  45259
 Copyright terms: Public domain W3C validator