Theorem ralbii 3133

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 339	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3131	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 209   ∈ wcel 2111  ∀wral 3106

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 3111

This theorem is referenced by:  2ralbii  3134  r19.26-2  3138  r19.26-3  3139  ralbiim  3141  dfral2  3200  ralnex2  3221  ralinexa  3223  rexanali  3224  nrexralim  3225  nelb  3227  r19.23v  3238  r19.32v  3294  ralcom13  3312  ralrot3  3314  cbvral2vw  3408  cbvral3vw  3410  cbvral2v  3411  cbvral3v  3413  sbralie  3418  ralcom4OLD  3472  ralxpxfr2d  3587  reu8  3672  2reuswap  3685  2reu5lem2  3695  2rmoswap  3700  rmoanim  3823  rmoanimALT  3824  dfss5  4191  n0el  4275  ralnralall  4416  2reu4lem  4423  r19.12sn  4616  raldifsnb  4689  eqsn  4722  n0snor2el  4724  uni0b  4826  uni0c  4827  ssint  4854  iuniin  4893  iuneq2  4900  iunssf  4931  iunss  4932  ssiinf  4941  iinab  4953  iinun2  4958  iindif1  4960  iindif2  4962  iinin2  4963  iinuni  4983  sspwuni  4985  iinpw  4991  disjor  5010  disjxun  5028  dftr3  5140  reusv3  5271  otiunsndisj  5375  ssrel2  5623  reliun  5653  xpiindi  5670  rexiunxp  5675  ralxpf  5681  rexxpf  5682  dfse2  5930  idrefALT  5940  asymref2  5944  rninxp  6003  dminxp  6004  cnviin  6105  cnvpo  6106  wfis2fg  6153  dffun9  6353  funcnv3  6394  fncnv  6397  fnres  6446  mptfnf  6455  fnopabg  6457  mptfng  6459  fint  6532  funimass4  6705  fndmdifeq0  6791  funconstss  6803  f1ompt  6852  idref  6885  fconstfv  6952  dff13f  6992  dff14b  7007  weniso  7086  foov  7302  dfwe2  7476  tfis2f  7550  tfindes  7557  frxp  7803  tz7.48lem  8060  tz7.49  8064  oeordi  8196  ixpeq2  8458  ixpin  8470  ixpiin  8471  boxriin  8487  findcard3  8745  fimax2g  8748  fissuni  8813  indexfi  8816  dfsup2  8892  sup0riota  8913  infcllem  8935  wemapsolem  8998  zfinf2  9089  oemapso  9129  zfregs2  9159  r1elss  9219  rankc1  9283  cp  9304  bnd2  9306  aceq1  9528  aceq2  9530  kmlem7  9567  kmlem12  9572  kmlem13  9573  kmlem15  9575  fin12  9824  ac6num  9890  ac6s2  9897  ac6sf  9900  ac6s4  9901  zorn2lem4  9910  zorn2lem6  9912  zorn2lem7  9913  zorng  9915  ttukeylem6  9925  brdom7disj  9942  brdom6disj  9943  fpwwe2  10054  fpwwe  10057  axgroth5  10235  axgroth4  10243  grothprim  10245  nqereu  10340  dfinfre  11609  infrenegsup  11611  xrsupsslem  12688  xrinfmsslem  12689  xrinfmss2  12692  fzshftral  12990  fsuppmapnn0ub  13358  mptnn0fsuppr  13362  hashgt12el  13779  hashgt12el2  13780  hashbc  13807  s3iunsndisj  14319  cotr2g  14327  rexfiuz  14699  clim0  14855  rpnnen2lem12  15570  gcdcllem1  15838  absproddvds  15951  coprmproddvdslem  15996  vdwmc2  16305  vdwlem13  16319  vdwnn  16324  xpscf  16830  mreacs  16921  acsfn  16922  acsfn1  16924  acsfn2  16926  ispos2  17550  lublecllem  17590  oduglb  17741  odulub  17743  posglbd  17752  isnmnd  17907  gsumwspan  18003  smndex2dnrinv  18072  isnsg2  18300  oppgid  18476  oppgcntz  18484  efgval2  18842  iscyggen2  18993  iscyg3  18998  oppr1  19380  isnirred  19446  lssne0  19715  isdomn2  20065  iunocv  20370  islindf4  20527  pmatcollpw2lem  21382  isbasis2g  21553  basdif0  21558  tgval2  21561  ntreq0  21682  isclo2  21693  opnnei  21725  neiptopnei  21737  lmres  21905  ist1-3  21954  cmpcov2  21995  cmpsub  22005  is1stc2  22047  1stccn  22068  kgencn  22161  eltx  22173  txkgen  22257  fbun  22445  trfbas  22449  fbunfip  22474  trfil2  22492  isufil2  22513  fixufil  22527  hausflim  22586  txflf  22611  fclsopn  22619  alexsubALTlem3  22654  isclmp  23702  iscau3  23882  iscau4  23883  caucfil  23887  bcth3  23935  ovolgelb  24084  dyadmax  24202  itg2leub  24338  itg2cn  24367  plydivex  24893  vieta1  24908  lgseisenlem2  25960  pnt3  26196  tglowdim2ln  26445  axcontlem12  26769  elntg2  26779  numedglnl  26937  vtxd0nedgb  27278  wlkvtxedg  27433  pthd  27558  2pthdlem1  27716  clwlkclwwlk  27787  3pthdlem1  27949  frgrregord013  28180  grpoidinvlem3  28289  nmoubi  28555  lnon0  28581  adjsym  29616  nmopub  29691  nmfnleub  29708  cvbr2  30066  chpssati  30146  chrelat2i  30148  chrelat3  30154  mdsymlem8  30193  nelbOLD  30239  ralcom4f  30240  moel  30259  reuxfrdf  30262  uniinn0  30314  ssiun3  30322  disjnf  30333  disjorf  30342  disjunsn  30357  ac6sf2  30384  nn0min  30562  tosglblem  30682  archiabl  30877  eulerpartlems  31728  eulerpartlemr  31742  eulerpartlemn  31749  ballotlem7  31903  bnj110  32240  bnj92  32244  bnj539  32273  bnj540  32274  bnj580  32295  bnj978  32331  bnj1047  32355  bnj1128  32372  bnj1417  32423  bnj1421  32424  bnj1312  32440  bnj1498  32443  lfuhgr3  32479  subfacp1lem3  32542  cvmlift2lem1  32662  cvmlift2lem12  32674  satfv1  32723  fmlaomn0  32750  fmla0disjsuc  32758  fmlasucdisj  32759  untuni  33048  dfso3  33063  dfpo2  33104  elintfv  33120  setinds  33136  setinds2f  33137  elpotr  33139  dfon2lem7  33147  dfon2lem9  33149  frpoins2fg  33195  frins2fg  33202  soseq  33209  nosepon  33285  nomaxmo  33314  nosupbnd1lem4  33324  conway  33377  ssltun2  33383  etasslt  33387  slerec  33390  dfint3  33526  brlb  33529  filnetlem4  33842  bj-reabeq  34463  ctbssinf  34823  fvineqsneq  34829  pibt2  34834  phpreu  35041  ptrecube  35057  poimirlem1  35058  poimirlem25  35082  poimirlem26  35083  poimirlem27  35084  poimirlem30  35087  mblfinlem2  35095  ftc1anc  35138  inixp  35166  ac6gf  35170  heibor1lem  35247  heiborlem1  35249  iscrngo2  35435  ac6s3f  35609  3ralbii  35670  idinxpssinxp2  35735  n0elqs  35743  ineleq  35768  refrelcosslem  35862  refrelcoss3  35863  lpssat  36309  lssat  36312  lcvbr2  36318  lcvbr3  36319  lfl1  36366  lub0N  36485  glb0N  36489  atlrelat1  36617  hlrelat2  36699  ispsubsp2  37042  pclclN  37187  cdleme25cv  37654  tendoeq2  38070  cdlemk35  38208  setindtrs  39966  cllem0  40265  ss2iundf  40360  ntrneixb  40798  gneispace  40837  expandral  40998  ismnuprim  41002  undisjrab  41010  zfregs2VD  41547  disjinfi  41820  iuneqfzuz  41967  mccl  42240  limsupub  42346  limsuppnflem  42352  limsupre2lem  42366  lmbr3v  42387  liminfpnfuz  42458  xlimpnfxnegmnf2  42500  ioodvbdlimc1lem2  42574  ioodvbdlimc2lem  42576  dvnprodlem3  42590  fourierdlem103  42851  fourierdlem104  42852  sge0iunmpt  43057  meaiuninc3v  43123  hoidmvle  43239  issmff  43368  r19.32  43653  2rexrsb  43657  cbvral2  43658  2ralbiim  43660  2reu3  43666  2reu8i  43669  otiunsndisjX  43835  0nelsetpreimafv  43907  copisnmnd  44429  lindslinindsimp1  44866  lindslinindsimp2  44872  snlindsntor  44880  ldepslinc  44918  setrec1lem3  45219  aacllem  45329