Theorem ralbii 3116

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

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2	1	imbi2i 328	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3114	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 198   ∈ wcel 2050  ∀wral 3089

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772

This theorem depends on definitions:  df-bi 199  df-ral 3094

This theorem is referenced by:  2ralbii  3117  r19.26-2  3122  r19.26-3  3123  ralbiim  3125  r19.28vOLD  3138  dfral2  3185  ralnex2  3207  ralinexa  3211  rexanali  3212  nrexralim  3213  r19.23v  3225  r19.30OLD  3281  r19.32v  3282  ralcom13  3301  ralrot3  3303  cbvral2v  3393  cbvral3v  3395  sbralie  3398  ralcom4OLD  3447  ralxpxfr2d  3555  reu8  3637  2reuswap  3650  2reu5lem2  3657  2rmoswap  3662  rmoanim  3782  rmoanimALT  3783  dfss5  4129  n0el  4208  ralnralall  4341  2reu4lem  4348  r19.12sn  4530  raldifsnb  4603  eqsn  4636  n0snor2el  4638  uni0b  4737  uni0c  4738  ssint  4765  iuniin  4803  iuneq2  4810  iunss  4835  ssiinf  4844  iinab  4856  iinun2  4861  iindif1  4863  iindif2  4865  iinin2  4866  iinuni  4886  sspwuni  4888  iinpw  4894  disjor  4911  disjxun  4927  dftr3  5034  trintOLD  5047  reusv3  5159  otiunsndisj  5266  ssrel2  5509  reliun  5539  xpiindi  5556  rexiunxp  5561  ralxpf  5567  rexxpf  5568  dfse2  5803  idrefALT  5813  asymref2  5817  rninxp  5876  dminxp  5877  cnviin  5975  cnvpo  5976  wfis2fg  6023  dffun9  6217  funcnv3  6257  fncnv  6260  fnres  6306  mptfnf  6313  fnopabg  6315  mptfng  6317  fint  6387  funimass4  6560  fndmdifeq0  6639  funconstss  6651  f1ompt  6698  idref  6731  fconstfv  6801  dff13f  6839  dff14b  6854  weniso  6930  foov  7138  dfwe2  7312  tfis2f  7386  tfindes  7393  frxp  7625  tz7.48lem  7880  tz7.49  7884  oeordi  8014  ixpeq2  8273  ixpin  8284  ixpiin  8285  boxriin  8301  findcard3  8556  fimax2g  8559  fissuni  8624  indexfi  8627  dfsup2  8703  sup0riota  8724  infcllem  8746  wemapsolem  8809  zfinf2  8899  oemapso  8939  zfregs2  8969  r1elss  9029  rankc1  9093  cp  9114  bnd2  9116  aceq1  9337  aceq2  9339  kmlem7  9376  kmlem12  9381  kmlem13  9382  kmlem15  9384  fin12  9633  ac6num  9699  ac6s2  9706  ac6sf  9709  ac6s4  9710  zorn2lem4  9719  zorn2lem6  9721  zorn2lem7  9722  zorng  9724  ttukeylem6  9734  brdom7disj  9751  brdom6disj  9752  fpwwe2  9863  fpwwe  9866  axgroth5  10044  axgroth4  10052  grothprim  10054  nqereu  10149  dfinfre  11423  infrenegsup  11425  xrsupsslem  12516  xrinfmsslem  12517  xrinfmss2  12520  fzshftral  12811  fsuppmapnn0ub  13178  mptnn0fsuppr  13182  hashgt12el  13596  hashgt12el2  13597  hashbc  13624  s3iunsndisj  14189  cotr2g  14197  rexfiuz  14568  clim0  14724  rpnnen2lem12  15438  gcdcllem1  15708  absproddvds  15817  coprmproddvdslem  15862  vdwmc2  16171  vdwlem13  16185  vdwnn  16190  xpscf  16695  mreacs  16787  acsfn  16788  acsfn1  16790  acsfn2  16792  ispos2  17416  lublecllem  17456  oduglb  17607  odulub  17609  posglbd  17618  isnmnd  17766  gsumwspan  17852  isnsg2  18093  oppgid  18255  oppgcntz  18263  efgval2  18608  iscyggen2  18756  iscyg3  18761  oppr1  19107  isnirred  19173  lssne0  19444  isdomn2  19793  iunocv  20527  islindf4  20684  pmatcollpw2lem  21089  isbasis2g  21260  basdif0  21265  tgval2  21268  ntreq0  21389  isclo2  21400  opnnei  21432  neiptopnei  21444  lmres  21612  ist1-3  21661  cmpcov2  21702  cmpsub  21712  is1stc2  21754  1stccn  21775  kgencn  21868  eltx  21880  txkgen  21964  fbun  22152  trfbas  22156  fbunfip  22181  trfil2  22199  isufil2  22220  fixufil  22234  hausflim  22293  txflf  22318  fclsopn  22326  alexsubALTlem3  22361  isclmp  23404  iscau3  23584  iscau4  23585  caucfil  23589  bcth3  23637  ovolgelb  23784  dyadmax  23902  itg2leub  24038  itg2cn  24067  plydivex  24589  vieta1  24604  lgseisenlem2  25654  pnt3  25890  tglowdim2ln  26139  axcontlem12  26464  elntg2  26474  numedglnl  26632  vtxd0nedgb  26973  wlkvtxedg  27128  pthd  27258  2pthdlem1  27436  clwlkclwwlk  27508  clwlkclwwlkOLD  27509  3pthdlem1  27693  frgrregord013  27952  grpoidinvlem3  28060  nmoubi  28326  lnon0  28352  adjsym  29391  nmopub  29466  nmfnleub  29483  cvbr2  29841  chpssati  29921  chrelat2i  29923  chrelat3  29929  mdsymlem8  29968  ralcom4f  30015  moel  30034  uniinn0  30070  ssiun3  30079  disjnf  30087  disjorf  30095  disjunsn  30110  ac6sf2  30134  nn0min  30283  tosglblem  30385  archiabl  30490  eulerpartlems  31260  eulerpartlemr  31274  eulerpartlemn  31281  ballotlem7  31436  bnj110  31774  bnj92  31778  bnj539  31807  bnj540  31808  bnj580  31829  bnj978  31865  bnj1047  31887  bnj1128  31904  bnj1417  31955  bnj1421  31956  bnj1312  31972  bnj1498  31975  subfacp1lem3  32011  cvmlift2lem1  32131  cvmlift2lem12  32143  untuni  32452  dfso3  32467  dfpo2  32508  elintfv  32524  setinds  32540  setinds2f  32541  elpotr  32543  dfon2lem7  32551  dfon2lem9  32553  frpoins2fg  32600  frins2fg  32607  soseq  32614  nosepon  32690  nomaxmo  32719  nosupbnd1lem4  32729  conway  32782  ssltun2  32788  etasslt  32792  slerec  32795  dfint3  32931  brlb  32934  filnetlem4  33247  ctbssinf  34125  fvineqsneq  34131  pibt2  34136  phpreu  34314  ptrecube  34330  poimirlem1  34331  poimirlem25  34355  poimirlem26  34356  poimirlem27  34357  poimirlem30  34360  mblfinlem2  34368  ftc1anc  34413  inixp  34442  ac6gf  34446  heibor1lem  34526  heiborlem1  34528  iscrngo2  34714  ac6s3f  34890  3ralbii  34951  idinxpssinxp2  35016  n0elqs  35025  ineleq  35051  refrelcosslem  35144  refrelcoss3  35145  lpssat  35591  lssat  35594  lcvbr2  35600  lcvbr3  35601  lfl1  35648  lub0N  35767  glb0N  35771  atlrelat1  35899  hlrelat2  35981  ispsubsp2  36324  pclclN  36469  cdleme25cv  36936  tendoeq2  37352  cdlemk35  37490  setindtrs  39015  cllem0  39284  ss2iundf  39364  ntrneixb  39805  gneispace  39844  expandral  39998  ismnuprim  40002  undisjrab  40051  zfregs2VD  40591  iunssf  40771  disjinfi  40876  iuneqfzuz  41030  mccl  41308  limsupub  41414  limsuppnflem  41420  limsupre2lem  41434  lmbr3v  41455  liminfpnfuz  41526  xlimpnfxnegmnf2  41568  ioodvbdlimc1lem2  41645  ioodvbdlimc2lem  41647  dvnprodlem3  41661  fourierdlem103  41923  fourierdlem104  41924  sge0iunmpt  42129  meaiuninc3v  42195  hoidmvle  42311  issmff  42440  r19.32  42700  2rexrsb  42704  cbvral2  42705  2ralbiim  42707  2reu3  42713  2reu8i  42716  otiunsndisjX  42882  copisnmnd  43442  lindslinindsimp1  43877  lindslinindsimp2  43883  snlindsntor  43891  ldepslinc  43929  setrec1lem3  44157  aacllem  44267