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 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2146  ∀wral 3079

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841

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

This theorem is used 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  3342  cbvral2v  3356  cbvral3v  3358  ceqsralv  3493  ralxpxfr2d  3602  reu8  3693  2reuswap  3706  2reu5lem2  3716  2rmoswap  3721  rmoanim  3845  rmoanimALT  3846  dfdif3  4057  dfss5  4222  n0el  4314  ralnralall  4471  2reu4lem  4481  r19.12sn  4680  raldifsnb  4758  eqsn  4787  n0snor2el  4790  uni0b  4896  uni0c  4897  ssint  4926  iuniin  4966  iuneq2  4973  iunssf  5003  iunssfOLD  5004  iunss  5005  iunssOLD  5006  ssiinf  5015  iinab  5028  iinun2  5033  iindif1  5037  iindif2  5039  iinin2  5040  iinuni  5060  sspwuni  5062  iinpw  5068  disjor  5087  disjxun  5103  dftr3  5219  reusv3  5370  otiunsndisj  5496  ssrel2  5765  reliun  5798  xpiindi  5816  rexiunxp  5821  ralxpf  5828  rexxpf  5829  dfse2  6103  idrefALT  6112  asymref2  6116  rninxp  6176  dminxp  6177  cnviin  6295  cnvpo  6296  dfpo2  6305  dfse3  6345  frpoins2fg  6353  dffun9  6577  funcnv3  6618  fncnv  6621  fnres  6674  mptfnf  6682  fnopabg  6684  mptfng  6686  fint  6769  funimass4  6957  fndmdifeq0  7051  funconstss  7063  f1ompt  7119  idref  7157  fconstfv  7225  dff13f  7266  dff14b  7282  weniso  7371  fnssintima  7379  foov  7602  imaeqalov  7667  dfwe2  7795  tfis2f  7874  tfindes  7881  ovmptss  8112  frxp  8148  ralxp3f  8164  frpoins3xpg  8167  frpoins3xp3g  8168  xpord2indlem  8174  xpord3inddlem  8181  soseq  8186  tz7.48lemOLD  8462  tz7.49  8466  oeordi  8607  naddcllem  8696  naddunif  8714  naddasslem2  8716  ixpeq2  8950  ixpin  8962  ixpiin  8963  boxriin  8979  findcard3  9285  fimax2g  9288  fissuni  9357  indexfi  9360  dfsup2  9446  sup0riota  9468  infcllem  9490  wemapsolem  9554  zfinf2  9653  oemapso  9693  ttrclresv  9728  zfregs2  9744  setinds  9760  setinds2f  9761  frins2f  9767  r1elss  9824  rankc1  9897  elhf4  9922  cp  9964  bnd2  9966  setrec1lem3  9979  aceq1  10206  aceq2  10208  kmlem7  10245  kmlem12  10250  kmlem13  10251  kmlem15  10253  fin12  10501  ac6num  10567  ac6s2  10574  ac6sf  10577  ac6s4  10578  zorn2lem4  10587  zorn2lem6  10589  zorn2lem7  10590  zorng  10592  ttukeylem6  10602  brdom7disj  10620  brdom6disj  10621  fpwwe2  10738  fpwwe  10741  axgroth5  10919  axgroth4  10927  grothprim  10929  nqereu  11024  dfinfre  12308  infrenegsup  12310  xrsupsslem  13447  xrinfmsslem  13448  xrinfmss2  13451  fzshftral  13759  fsuppmapnn0ub  14148  mptnn0fsuppr  14152  hashgt12el  14577  hashgt12el2  14578  hashbc  14608  s3iunsndisj  15133  cotr2g  15141  rexfiuz  15527  clim0  15685  rpnnen2lem12  16405  gcdcllem1  16681  absproddvds  16804  coprmproddvdslem  16849  vdwmc2  17169  vdwlem13  17183  vdwnn  17188  xpscf  17749  mreacs  17844  acsfn  17845  acsfn1  17847  acsfn2  17849  dfinito2  18190  dftermo2  18191  ispos2  18501  lublecllem  18544  odulub  18591  oduglb  18593  posglbdg  18599  isnmnd  18939  gsumwspan  19054  smndex2dnrinv  19126  isnsg2  19378  oppgid  19582  oppgcntz  19590  efgval2  19950  iscyggen2  20107  iscyg3  20112  dfring3  20530  oppr1  20592  isnirred  20662  isdomn5  20974  lssne0  21238  iunocv  21999  islindf4  22156  pmatcollpw2lem  23107  isbasis2g  23278  basdif0  23283  tgval2  23286  ntreq0  23407  isclo2  23418  opnnei  23450  neiptopnei  23462  lmres  23630  ist1-3  23679  cmpcov2  23720  cmpsub  23730  is1stc2  23772  1stccn  23794  kgencn  23887  eltx  23899  txkgen  23983  fbun  24171  trfbas  24175  fbunfip  24200  trfil2  24218  isufil2  24239  fixufil  24253  hausflim  24312  txflf  24337  fclsopn  24345  alexsubALTlem3  24380  isclmp  25430  iscau3  25611  iscau4  25612  caucfil  25616  bcth3  25664  ovolgelb  25813  dyadmax  25931  itg2leub  26067  itg2cn  26096  plydivex  26630  vieta1  26647  lgseisenlem2  27715  pnt3  27951  infdesc  27979  nosepon  28034  nomaxmo  28067  nosupbnd1lem4  28080  conway  28177  eqcuts2  28184  etaslts  28191  lesrec  28197  bday1  28212  cuteq1  28215  madebdaylemlrcut  28297  addsproplem4  28370  addsproplem6  28372  addsprop  28374  addsuniflem  28399  mulsuniflem  28547  oncutlt  28662  oniso  28669  onsfi  28754  bdayn0p1  28767  addhalfcut  28857  tglowdim2ln  29132  axcontlem12  29565  elntg2  29575  numedglnl  29734  lfuhgr3  29740  vtxd0nedgb  30081  wlkvtxedg  30236  pthd  30367  2pthdlem1  30531  clwlkclwwlk  30605  3pthdlem1  30777  frgrregord013  31008  grpoidinvlem3  31120  nmoubi  31386  lnon0  31412  adjsym  32447  nmopub  32522  nmfnleub  32539  cvbr2  32897  chpssati  32977  chrelat2i  32979  chrelat3  32985  mdsymlem8  33024  ralcom4f  33118  reuxfrdf  33141  n0nsnel  33165  uniinn0  33201  ssiun3  33207  disjnf  33218  disjorf  33227  disjunsn  33242  ac6sf2  33270  acunirnmpt2f  33309  nn0min  33465  tosglblem  33588  archiabl  33812  1arithidom  34122  eulerpartlems  35045  eulerpartlemr  35059  eulerpartlemn  35066  ballotlem7  35221  bnj110  35541  bnj92  35545  bnj539  35574  bnj540  35575  bnj580  35596  bnj978  35632  bnj1047  35656  bnj1128  35673  bnj1417  35724  bnj1421  35725  bnj1312  35741  bnj1498  35744  fwfffun  35770  r1omhf  35792  rankse  35802  onvf1od  35989  subfacp1lem3  36068  cvmlift2lem1  36188  cvmlift2lem12  36200  satfv1  36249  fmlaomn0  36276  fmla0disjsuc  36284  fmlasucdisj  36285  untuni  36601  dfso3  36612  dffr5  36646  elintfv  36657  elpotr  36670  dfon2lem7  36678  dfon2lem9  36680  dfint3  36843  brlb  36846  dffr7  36847  filnetlem4  37296  axtco  37386  axtco1g  37391  regsfromregtco  37453  mh-infprim3bi  37463  bj-reabeq  38067  bj-axseprep  38129  ctbssinf  38469  fvineqsneq  38475  pibt2  38480  phpreu  38667  ptrecube  38678  poimirlem1  38679  poimirlem25  38703  poimirlem26  38704  poimirlem27  38705  poimirlem30  38708  mblfinlem2  38716  ftc1anc  38759  inixp  38802  ac6gf  38806  heibor1lem  38883  heiborlem1  38885  iscrngo2  39071  ac6s3f  39243  ref5  39391  idinxpssinxp2  39396  n0elqs  39404  ineleq  39426  ralrnmo  39433  ssdmral  39451  refrelcosslem  39624  refrelcoss3  39625  lpssat  40210  lssat  40213  lcvbr2  40219  lcvbr3  40220  lfl1  40267  lub0N  40386  glb0N  40390  atlrelat1  40518  hlrelat2  40600  ispsubsp2  40943  pclclN  41088  cdleme25cv  41555  tendoeq2  41971  cdlemk35  42109  aks4d1p7  43273  sticksstones1  43336  indstrd  43383  supinf  43433  frlmnzcoordex  43792  setindtrs  44172  unielss  44360  ssunib  44362  onsupmaxb  44381  onsupeqnmax  44389  cllem0  44707  ntrneixb  45235  gneispace  45274  expandral  45414  ismnuprim  45418  dfuniv2  45426  undisjrab  45430  zfregs2VD  45962  sswfaxreg  46116  dfac5prim  46119  permac8prim  46143  iindif2f  46314  ralfal  46315  disjinfi  46346  iuneqfzuz  46486  caucvgbf  46638  rexanuz2nf  46641  mccl  46749  limsupub  46853  limsuppnflem  46859  limsupre2lem  46873  lmbr3v  46894  liminfpnfuz  46965  xlimpnfxnegmnf2  47007  ioodvbdlimc1lem2  47081  ioodvbdlimc2lem  47083  dvnprodlem3  47097  fourierdlem103  47358  fourierdlem104  47359  sge0iunmpt  47567  meaiuninc3v  47633  hoidmvle  47749  issmff  47883  n0nsn2el  48234  r19.32  48308  2rexrsb  48312  cbvral2  48313  2reu3  48320  2reu8i  48323  otiunsndisjX  48488  0nelsetpreimafv  48611  dfgric2  49152  gpg5nbgrvtx03starlem1  49305  gpg5nbgrvtx03starlem2  49306  gpg5nbgrvtx03starlem3  49307  gpg5nbgrvtx13starlem1  49308  gpg5nbgrvtx13starlem2  49309  gpg5nbgrvtx13starlem3  49310  gpg5edgnedg  49367  copisnmnd  49405  lindslinindsimp1  49708  lindslinindsimp2  49714  snlindsntor  49722  ldepslinc  49760  iuneq0  50069  iinxp  50081  iscnrm3  50205  ralsbii  51111  ralseubii  51143  aacllem  51153