Theorem ralbii 3082

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

Syntax hints:   ↔ wb 205   ∈ wcel 2098  ∀wral 3050

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

This theorem depends on definitions:  df-bi 206  df-ral 3051

This theorem is referenced by:  dfral2  3088  ralinexa  3090  rexanali  3091  rexbiOLD  3094  r19.26-3  3101  ralbiim  3102  2ralbii  3117  3ralbii  3119  4ralbii  3120  2ralbiim  3121  ralnex2  3122  nrexralim  3126  r19.26-2  3127  r19.23v  3172  r19.32v  3181  2ralor  3218  nelb  3221  nelbOLD  3222  cbvral2vw  3228  cbvral3vw  3230  ralrot3  3280  ralcom13  3281  ralcom13OLD  3282  sbralieALT  3342  cbvral2v  3351  cbvral3v  3353  moelOLD  3388  ceqsralv  3503  ralxpxfr2d  3630  reu8  3726  2reuswap  3739  2reu5lem2  3749  2rmoswap  3754  rmoanim  3886  rmoanimALT  3887  dfss5  4265  n0el  4363  ralnralall  4522  2reu4lem  4529  r19.12sn  4728  raldifsnb  4804  eqsn  4837  n0snor2el  4839  uni0b  4940  uni0c  4941  ssint  4971  iuniin  5012  iuneq2  5019  iunssf  5051  iunss  5052  ssiinf  5061  iinab  5075  iinun2  5080  iindif1  5082  iindif2  5084  iinin2  5085  iinuni  5105  sspwuni  5107  iinpw  5113  disjor  5132  disjxun  5150  dftr3  5275  reusv3  5408  otiunsndisj  5525  ssrel2  5790  reliun  5821  xpiindi  5841  rexiunxp  5846  ralxpf  5852  rexxpf  5853  dfse2  6109  idrefALT  6122  asymref2  6128  rninxp  6189  dminxp  6190  cnviin  6296  cnvpo  6297  dfpo2  6306  dfse3  6348  frpoins2fg  6356  wfis2fgOLD  6369  dffun9  6587  funcnv3  6628  fncnv  6631  fnres  6687  mptfnf  6695  fnopabg  6697  mptfng  6699  fint  6780  funimass4  6966  fndmdifeq0  7056  funconstss  7068  f1ompt  7124  idref  7159  fconstfv  7228  dff13f  7270  dff14b  7285  weniso  7365  fnssintima  7373  foov  7599  imaeqalov  7664  dfwe2  7781  tfis2f  7865  tfindes  7872  frxp  8139  ralxp3f  8150  frpoins3xpg  8153  frpoins3xp3g  8154  xpord2indlem  8160  xpord3inddlem  8167  soseq  8172  dfwrecsOLD  8327  tz7.48lem  8470  tz7.49  8474  oeordi  8616  naddcllem  8705  naddunif  8722  naddasslem2  8724  ixpeq2  8939  ixpin  8951  ixpiin  8952  boxriin  8968  findcard3  9322  findcard3OLD  9323  fimax2g  9326  fissuni  9397  indexfi  9400  dfsup2  9483  sup0riota  9504  infcllem  9526  wemapsolem  9589  zfinf2  9681  oemapso  9721  ttrclresv  9756  zfregs2  9772  frins2f  9792  r1elss  9845  rankc1  9909  cp  9930  bnd2  9932  aceq1  10156  aceq2  10158  kmlem7  10195  kmlem12  10200  kmlem13  10201  kmlem15  10203  fin12  10452  ac6num  10518  ac6s2  10525  ac6sf  10528  ac6s4  10529  zorn2lem4  10538  zorn2lem6  10540  zorn2lem7  10541  zorng  10543  ttukeylem6  10553  brdom7disj  10570  brdom6disj  10571  fpwwe2  10682  fpwwe  10685  axgroth5  10863  axgroth4  10871  grothprim  10873  nqereu  10968  dfinfre  12242  infrenegsup  12244  xrsupsslem  13335  xrinfmsslem  13336  xrinfmss2  13339  fzshftral  13638  fsuppmapnn0ub  14010  mptnn0fsuppr  14014  hashgt12el  14434  hashgt12el2  14435  hashbc  14465  s3iunsndisj  14968  cotr2g  14976  rexfiuz  15347  clim0  15503  rpnnen2lem12  16222  gcdcllem1  16494  absproddvds  16613  coprmproddvdslem  16658  vdwmc2  16976  vdwlem13  16990  vdwnn  16995  xpscf  17575  mreacs  17666  acsfn  17667  acsfn1  17669  acsfn2  17671  dfinito2  18020  dftermo2  18021  ispos2  18335  lublecllem  18380  odulub  18427  oduglb  18429  posglbdg  18435  isnmnd  18726  gsumwspan  18831  smndex2dnrinv  18900  isnsg2  19145  oppgid  19348  oppgcntz  19356  efgval2  19717  iscyggen2  19874  iscyg3  19879  oppr1  20327  isnirred  20397  lssne0  20875  isdomn5  21293  isdomn2OLD  21295  iunocv  21669  islindf4  21828  pmatcollpw2lem  22762  isbasis2g  22934  basdif0  22939  tgval2  22942  ntreq0  23064  isclo2  23075  opnnei  23107  neiptopnei  23119  lmres  23287  ist1-3  23336  cmpcov2  23377  cmpsub  23387  is1stc2  23429  1stccn  23450  kgencn  23543  eltx  23555  txkgen  23639  fbun  23827  trfbas  23831  fbunfip  23856  trfil2  23874  isufil2  23895  fixufil  23909  hausflim  23968  txflf  23993  fclsopn  24001  alexsubALTlem3  24036  isclmp  25107  iscau3  25289  iscau4  25290  caucfil  25294  bcth3  25342  ovolgelb  25492  dyadmax  25610  itg2leub  25747  itg2cn  25776  plydivex  26317  vieta1  26332  lgseisenlem2  27397  pnt3  27633  nosepon  27687  nomaxmo  27720  nosupbnd1lem4  27733  conway  27821  eqscut2  27828  etasslt  27835  slerec  27841  bday1s  27853  cuteq1  27855  madebdaylemlrcut  27914  addsproplem4  27978  addsproplem6  27980  addsprop  27982  addsuniflem  28007  mulsuniflem  28142  tglowdim2ln  28570  axcontlem12  28901  elntg2  28911  numedglnl  29072  vtxd0nedgb  29417  wlkvtxedg  29573  pthd  29698  2pthdlem1  29856  clwlkclwwlk  29927  3pthdlem1  30089  frgrregord013  30320  grpoidinvlem3  30431  nmoubi  30697  lnon0  30723  adjsym  31758  nmopub  31833  nmfnleub  31850  cvbr2  32208  chpssati  32288  chrelat2i  32290  chrelat3  32296  mdsymlem8  32335  ralcom4f  32388  reuxfrdf  32410  n0nsnel  32432  uniinn0  32462  ssiun3  32470  disjnf  32481  disjorf  32490  disjunsn  32505  ac6sf2  32533  nn0min  32710  tosglblem  32832  archiabl  33040  1arithidom  33389  eulerpartlems  34150  eulerpartlemr  34164  eulerpartlemn  34171  ballotlem7  34325  bnj110  34659  bnj92  34663  bnj539  34692  bnj540  34693  bnj580  34714  bnj978  34750  bnj1047  34774  bnj1128  34791  bnj1417  34842  bnj1421  34843  bnj1312  34859  bnj1498  34862  lfuhgr3  34899  subfacp1lem3  34962  cvmlift2lem1  35082  cvmlift2lem12  35094  satfv1  35143  fmlaomn0  35170  fmla0disjsuc  35178  fmlasucdisj  35179  untuni  35479  dfso3  35490  elintfv  35536  setinds  35550  setinds2f  35551  elpotr  35553  dfon2lem7  35561  dfon2lem9  35563  dfint3  35724  brlb  35727  filnetlem4  36041  bj-reabeq  36682  ctbssinf  37061  fvineqsneq  37067  pibt2  37072  phpreu  37253  ptrecube  37269  poimirlem1  37270  poimirlem25  37294  poimirlem26  37295  poimirlem27  37296  poimirlem30  37299  mblfinlem2  37307  ftc1anc  37350  inixp  37377  ac6gf  37381  heibor1lem  37458  heiborlem1  37460  iscrngo2  37646  ac6s3f  37820  ref5  37959  idinxpssinxp2  37964  n0elqs  37972  ineleq  38000  refrelcosslem  38108  refrelcoss3  38109  lpssat  38659  lssat  38662  lcvbr2  38668  lcvbr3  38669  lfl1  38716  lub0N  38835  glb0N  38839  atlrelat1  38967  hlrelat2  39050  ispsubsp2  39393  pclclN  39538  cdleme25cv  40005  tendoeq2  40421  cdlemk35  40559  aks4d1p7  41730  sticksstones1  41792  infdesc  42234  setindtrs  42620  unielss  42820  ssunib  42822  onsupmaxb  42841  onsupeqnmax  42849  cllem0  43170  ntrneixb  43699  gneispace  43738  expandral  43901  ismnuprim  43905  dfuniv2  43913  undisjrab  43917  zfregs2VD  44454  iindif2f  44702  ralfal  44703  disjinfi  44736  iuneqfzuz  44887  caucvgbf  45042  rexanuz2nf  45045  mccl  45156  limsupub  45262  limsuppnflem  45268  limsupre2lem  45282  lmbr3v  45303  liminfpnfuz  45374  xlimpnfxnegmnf2  45416  ioodvbdlimc1lem2  45490  ioodvbdlimc2lem  45492  dvnprodlem3  45506  fourierdlem103  45767  fourierdlem104  45768  sge0iunmpt  45976  meaiuninc3v  46042  hoidmvle  46158  issmff  46292  n0nsn2el  46577  r19.32  46648  2rexrsb  46652  cbvral2  46653  2reu3  46660  2reu8i  46663  otiunsndisjX  46829  0nelsetpreimafv  46899  dfgric2  47400  copisnmnd  47483  lindslinindsimp1  47777  lindslinindsimp2  47783  snlindsntor  47791  ldepslinc  47829  iscnrm3  48223  setrec1lem3  48372  aacllem  48486