Theorem ralbii 3111

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	a1i 11	. 2 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
3	2	ralbiia 3109	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 209   ∈ wcel 2143  ∀wral 3079

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

This theorem depends on definitions:  df-bi 210  df-ral 3080

This theorem is referenced by:  dfral2  3116  ralinexa  3118  rexanali  3119  r19.26-3  3126  ralbiim  3127  2ralbii  3140  3ralbii  3142  4ralbii  3143  2ralbiim  3144  ralnex2  3145  nrexralim  3149  r19.26-2  3150  r19.23v  3192  r19.32v  3198  2ralor  3239  nelb  3241  cbvral2vw  3247  cbvral3vw  3249  ralrot3  3296  ralcom13  3297  sbralieALT  3343  cbvral2v  3357  cbvral3v  3359  ceqsralv  3495  ralxpxfr2d  3605  reu8  3696  2reuswap  3709  2reu5lem2  3719  2rmoswap  3724  rmoanim  3848  rmoanimALT  3849  dfdif3  4072  dfss5  4228  n0el  4319  ralnralall  4474  2reu4lem  4484  r19.12sn  4686  raldifsnb  4764  eqsn  4795  n0snor2el  4798  uni0b  4899  uni0c  4900  ssint  4929  iuniin  4969  iuneq2  4976  iunssf  5007  iunssfOLD  5008  iunss  5009  iunssOLD  5010  ssiinf  5019  iinab  5032  iinun2  5037  iindif1  5041  iindif2  5043  iinin2  5044  iinuni  5064  sspwuni  5066  iinpw  5072  disjor  5091  disjxun  5107  dftr3  5223  reusv3  5376  otiunsndisj  5503  ssrel2  5771  reliun  5803  xpiindi  5821  rexiunxp  5826  ralxpf  5832  rexxpf  5833  dfse2  6102  idrefALT  6113  asymref2  6117  rninxp  6177  dminxp  6178  cnviin  6287  cnvpo  6288  dfpo2  6297  dfse3  6337  frpoins2fg  6345  dffun9  6565  funcnv3  6606  fncnv  6609  fnres  6662  mptfnf  6670  fnopabg  6672  mptfng  6674  fint  6757  funimass4  6945  fndmdifeq0  7039  funconstss  7051  f1ompt  7106  idref  7142  fconstfv  7210  dff13f  7253  dff14b  7269  weniso  7352  fnssintima  7360  foov  7584  imaeqalov  7649  dfwe2  7769  tfis2f  7848  tfindes  7855  frxp  8118  ralxp3f  8129  frpoins3xpg  8132  frpoins3xp3g  8133  xpord2indlem  8139  xpord3inddlem  8146  soseq  8151  tz7.48lem  8424  tz7.49  8428  oeordi  8569  naddcllem  8658  naddunif  8676  naddasslem2  8678  ixpeq2  8905  ixpin  8917  ixpiin  8918  boxriin  8934  findcard3  9239  fimax2g  9242  fissuni  9310  indexfi  9313  dfsup2  9400  sup0riota  9422  infcllem  9444  wemapsolem  9508  zfinf2  9607  oemapso  9647  ttrclresv  9682  zfregs2  9698  setinds  9714  setinds2f  9715  frins2f  9721  r1elss  9774  rankc1  9838  cp  9873  bnd2  9875  aceq1  10097  aceq2  10099  kmlem7  10136  kmlem12  10141  kmlem13  10142  kmlem15  10144  fin12  10392  ac6num  10458  ac6s2  10465  ac6sf  10468  ac6s4  10469  zorn2lem4  10478  zorn2lem6  10480  zorn2lem7  10481  zorng  10483  ttukeylem6  10493  brdom7disj  10510  brdom6disj  10511  fpwwe2  10623  fpwwe  10626  axgroth5  10804  axgroth4  10812  grothprim  10814  nqereu  10909  dfinfre  12191  infrenegsup  12193  xrsupsslem  13328  xrinfmsslem  13329  xrinfmss2  13332  fzshftral  13639  fsuppmapnn0ub  14027  mptnn0fsuppr  14031  hashgt12el  14455  hashgt12el2  14456  hashbc  14486  s3iunsndisj  15001  cotr2g  15009  rexfiuz  15395  clim0  15553  rpnnen2lem12  16276  gcdcllem1  16552  absproddvds  16670  coprmproddvdslem  16715  vdwmc2  17034  vdwlem13  17048  vdwnn  17053  xpscf  17614  mreacs  17709  acsfn  17710  acsfn1  17712  acsfn2  17714  dfinito2  18055  dftermo2  18056  ispos2  18366  lublecllem  18409  odulub  18456  oduglb  18458  posglbdg  18464  isnmnd  18791  gsumwspan  18900  smndex2dnrinv  18972  isnsg2  19217  oppgid  19421  oppgcntz  19429  efgval2  19789  iscyggen2  19946  iscyg3  19951  oppr1  20428  isnirred  20498  isdomn5  20809  lssne0  21072  iunocv  21831  islindf4  21988  pmatcollpw2lem  22934  isbasis2g  23105  basdif0  23110  tgval2  23113  ntreq0  23234  isclo2  23245  opnnei  23277  neiptopnei  23289  lmres  23457  ist1-3  23506  cmpcov2  23547  cmpsub  23557  is1stc2  23599  1stccn  23620  kgencn  23713  eltx  23725  txkgen  23809  fbun  23997  trfbas  24001  fbunfip  24026  trfil2  24044  isufil2  24065  fixufil  24079  hausflim  24138  txflf  24163  fclsopn  24171  alexsubALTlem3  24206  isclmp  25256  iscau3  25437  iscau4  25438  caucfil  25442  bcth3  25490  ovolgelb  25639  dyadmax  25757  itg2leub  25893  itg2cn  25922  plydivex  26458  vieta1  26473  lgseisenlem2  27540  pnt3  27776  nosepon  27829  nomaxmo  27862  nosupbnd1lem4  27875  conway  27972  eqcuts2  27979  etaslts  27986  lesrec  27992  bday1  28007  cuteq1  28010  madebdaylemlrcut  28092  addsproplem4  28165  addsproplem6  28167  addsprop  28169  addsuniflem  28194  mulsuniflem  28342  oncutlt  28457  oniso  28464  onsfi  28549  bdayn0p1  28562  addhalfcut  28652  tglowdim2ln  28925  axcontlem12  29325  elntg2  29335  numedglnl  29494  vtxd0nedgb  29838  wlkvtxedg  29993  pthd  30118  2pthdlem1  30279  clwlkclwwlk  30353  3pthdlem1  30515  frgrregord013  30746  grpoidinvlem3  30858  nmoubi  31124  lnon0  31150  adjsym  32185  nmopub  32260  nmfnleub  32277  cvbr2  32635  chpssati  32715  chrelat2i  32717  chrelat3  32723  mdsymlem8  32762  ralcom4f  32814  reuxfrdf  32837  n0nsnel  32861  uniinn0  32897  ssiun3  32903  disjnf  32915  disjorf  32924  disjunsn  32939  ac6sf2  32967  nn0min  33165  tosglblem  33294  archiabl  33518  1arithidom  33827  eulerpartlems  34750  eulerpartlemr  34764  eulerpartlemn  34771  ballotlem7  34926  bnj110  35246  bnj92  35250  bnj539  35279  bnj540  35280  bnj580  35301  bnj978  35337  bnj1047  35361  bnj1128  35378  bnj1417  35429  bnj1421  35430  bnj1312  35446  bnj1498  35449  onvf1od  35591  lfuhgr3  35612  subfacp1lem3  35674  cvmlift2lem1  35794  cvmlift2lem12  35806  satfv1  35855  fmlaomn0  35882  fmla0disjsuc  35890  fmlasucdisj  35891  untuni  36201  dfso3  36212  elintfv  36257  elpotr  36271  dfon2lem7  36279  dfon2lem9  36281  dfint3  36444  brlb  36447  filnetlem4  36912  axtco  37002  axtco1g  37007  regsfromregtco  37069  mh-infprim3bi  37079  bj-reabeq  37683  bj-axseprep  37731  ctbssinf  38072  fvineqsneq  38078  pibt2  38083  phpreu  38275  ptrecube  38291  poimirlem1  38292  poimirlem25  38316  poimirlem26  38317  poimirlem27  38318  poimirlem30  38321  mblfinlem2  38329  ftc1anc  38372  inixp  38399  ac6gf  38403  heibor1lem  38480  heiborlem1  38482  iscrngo2  38668  ac6s3f  38840  ref5  38988  idinxpssinxp2  38993  n0elqs  39001  ineleq  39023  ralrnmo  39030  ssdmral  39048  refrelcosslem  39221  refrelcoss3  39222  lpssat  39807  lssat  39810  lcvbr2  39816  lcvbr3  39817  lfl1  39864  lub0N  39983  glb0N  39987  atlrelat1  40115  hlrelat2  40197  ispsubsp2  40540  pclclN  40685  cdleme25cv  41152  tendoeq2  41568  cdlemk35  41706  aks4d1p7  42870  sticksstones1  42933  indstrd  42980  supinf  43030  infdesc  43395  setindtrs  43772  unielss  43965  ssunib  43967  onsupmaxb  43986  onsupeqnmax  43994  cllem0  44312  ntrneixb  44841  gneispace  44880  expandral  45020  ismnuprim  45024  dfuniv2  45032  undisjrab  45036  zfregs2VD  45569  sswfaxreg  45716  dfac5prim  45719  permac8prim  45743  iindif2f  45898  ralfal  45899  disjinfi  45930  iuneqfzuz  46071  caucvgbf  46223  rexanuz2nf  46226  mccl  46334  limsupub  46438  limsuppnflem  46444  limsupre2lem  46458  lmbr3v  46479  liminfpnfuz  46550  xlimpnfxnegmnf2  46592  ioodvbdlimc1lem2  46666  ioodvbdlimc2lem  46668  dvnprodlem3  46682  fourierdlem103  46943  fourierdlem104  46944  sge0iunmpt  47152  meaiuninc3v  47218  hoidmvle  47334  issmff  47468  n0nsn2el  47782  r19.32  47855  2rexrsb  47859  cbvral2  47860  2reu3  47867  2reu8i  47870  otiunsndisjX  48036  0nelsetpreimafv  48159  dfgric2  48700  gpg5nbgrvtx03starlem1  48853  gpg5nbgrvtx03starlem2  48854  gpg5nbgrvtx03starlem3  48855  gpg5nbgrvtx13starlem1  48856  gpg5nbgrvtx13starlem2  48857  gpg5nbgrvtx13starlem3  48858  gpg5edgnedg  48915  copisnmnd  48954  lindslinindsimp1  49257  lindslinindsimp2  49263  snlindsntor  49271  ldepslinc  49309  iuneq0  49617  iinxp  49629  iscnrm3  49750  setrec1lem3  50487  ralsbii  50599  ralseubii  50631  aacllem  50641