Theorem ralbii 3117

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

Syntax hints:   ↔ wb 209   ∈ wcel 2149  ∀wral 3085

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

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

This theorem is referenced by:  dfral2  3122  ralinexa  3124  rexanali  3125  r19.26-3  3132  ralbiim  3133  2ralbii  3146  3ralbii  3148  4ralbii  3149  2ralbiim  3150  ralnex2  3151  nrexralim  3155  r19.26-2  3156  r19.23v  3198  r19.32v  3204  2ralor  3245  nelb  3247  cbvral2vw  3253  cbvral3vw  3255  ralrot3  3302  ralcom13  3303  sbralieALT  3350  cbvral2v  3364  cbvral3v  3366  ceqsralv  3503  ralxpxfr2d  3614  reu8  3705  2reuswap  3718  2reu5lem2  3728  2rmoswap  3733  rmoanim  3856  rmoanimALT  3857  dfdif3  4080  dfss5  4236  n0el  4327  ralnralall  4479  2reu4lem  4489  r19.12sn  4691  raldifsnb  4768  eqsn  4799  n0snor2el  4802  uni0b  4903  uni0c  4904  ssint  4933  iuniin  4973  iuneq2  4980  iunssf  5011  iunssfOLD  5012  iunss  5013  iunssOLD  5014  ssiinf  5023  iinab  5036  iinun2  5041  iindif1  5045  iindif2  5047  iinin2  5048  iinuni  5068  sspwuni  5070  iinpw  5076  disjor  5095  disjxun  5111  dftr3  5227  reusv3  5377  otiunsndisj  5504  ssrel2  5772  reliun  5804  xpiindi  5822  rexiunxp  5827  ralxpf  5833  rexxpf  5834  dfse2  6103  idrefALT  6114  asymref2  6118  rninxp  6178  dminxp  6179  cnviin  6288  cnvpo  6289  dfpo2  6298  dfse3  6338  frpoins2fg  6346  dffun9  6566  funcnv3  6607  fncnv  6610  fnres  6663  mptfnf  6671  fnopabg  6673  mptfng  6675  fint  6758  funimass4  6946  fndmdifeq0  7040  funconstss  7052  f1ompt  7107  idref  7143  fconstfv  7211  dff13f  7254  dff14b  7270  weniso  7353  fnssintima  7361  foov  7585  imaeqalov  7650  dfwe2  7772  tfis2f  7851  tfindes  7858  frxp  8121  ralxp3f  8132  frpoins3xpg  8135  frpoins3xp3g  8136  xpord2indlem  8142  xpord3inddlem  8149  soseq  8154  tz7.48lem  8427  tz7.49  8431  oeordi  8572  naddcllem  8661  naddunif  8679  naddasslem2  8681  ixpeq2  8908  ixpin  8920  ixpiin  8921  boxriin  8937  findcard3  9242  fimax2g  9245  fissuni  9313  indexfi  9316  dfsup2  9403  sup0riota  9425  infcllem  9447  wemapsolem  9511  zfinf2  9610  oemapso  9650  ttrclresv  9685  zfregs2  9701  setinds  9717  setinds2f  9718  frins2f  9724  r1elss  9777  rankc1  9841  cp  9876  bnd2  9878  aceq1  10100  aceq2  10102  kmlem7  10139  kmlem12  10144  kmlem13  10145  kmlem15  10147  fin12  10396  ac6num  10462  ac6s2  10469  ac6sf  10472  ac6s4  10473  zorn2lem4  10482  zorn2lem6  10484  zorn2lem7  10485  zorng  10487  ttukeylem6  10497  brdom7disj  10514  brdom6disj  10515  fpwwe2  10627  fpwwe  10630  axgroth5  10808  axgroth4  10816  grothprim  10818  nqereu  10913  dfinfre  12195  infrenegsup  12197  xrsupsslem  13332  xrinfmsslem  13333  xrinfmss2  13336  fzshftral  13642  fsuppmapnn0ub  14030  mptnn0fsuppr  14034  hashgt12el  14458  hashgt12el2  14459  hashbc  14489  s3iunsndisj  15004  cotr2g  15012  rexfiuz  15398  clim0  15556  rpnnen2lem12  16280  gcdcllem1  16556  absproddvds  16674  coprmproddvdslem  16719  vdwmc2  17038  vdwlem13  17052  vdwnn  17057  xpscf  17618  mreacs  17713  acsfn  17714  acsfn1  17716  acsfn2  17718  dfinito2  18059  dftermo2  18060  ispos2  18370  lublecllem  18413  odulub  18460  oduglb  18462  posglbdg  18468  isnmnd  18795  gsumwspan  18904  smndex2dnrinv  18976  isnsg2  19221  oppgid  19425  oppgcntz  19433  efgval2  19793  iscyggen2  19950  iscyg3  19955  oppr1  20431  isnirred  20501  isdomn5  20794  lssne0  21049  iunocv  21799  islindf4  21956  pmatcollpw2lem  22902  isbasis2g  23073  basdif0  23078  tgval2  23081  ntreq0  23202  isclo2  23213  opnnei  23245  neiptopnei  23257  lmres  23425  ist1-3  23474  cmpcov2  23515  cmpsub  23525  is1stc2  23567  1stccn  23588  kgencn  23681  eltx  23693  txkgen  23777  fbun  23965  trfbas  23969  fbunfip  23994  trfil2  24012  isufil2  24033  fixufil  24047  hausflim  24106  txflf  24131  fclsopn  24139  alexsubALTlem3  24174  isclmp  25224  iscau3  25405  iscau4  25406  caucfil  25410  bcth3  25458  ovolgelb  25607  dyadmax  25725  itg2leub  25861  itg2cn  25890  plydivex  26426  vieta1  26441  lgseisenlem2  27505  pnt3  27741  nosepon  27794  nomaxmo  27827  nosupbnd1lem4  27840  conway  27937  eqcuts2  27944  etaslts  27951  lesrec  27957  bday1  27972  cuteq1  27975  madebdaylemlrcut  28057  addsproplem4  28130  addsproplem6  28132  addsprop  28134  addsuniflem  28159  mulsuniflem  28307  oncutlt  28422  oniso  28429  onsfi  28514  bdayn0p1  28527  addhalfcut  28617  tglowdim2ln  28886  axcontlem12  29265  elntg2  29275  numedglnl  29434  vtxd0nedgb  29778  wlkvtxedg  29933  pthd  30058  2pthdlem1  30219  clwlkclwwlk  30293  3pthdlem1  30455  frgrregord013  30686  grpoidinvlem3  30798  nmoubi  31064  lnon0  31090  adjsym  32125  nmopub  32200  nmfnleub  32217  cvbr2  32575  chpssati  32655  chrelat2i  32657  chrelat3  32663  mdsymlem8  32702  ralcom4f  32754  reuxfrdf  32777  n0nsnel  32801  uniinn0  32837  ssiun3  32843  disjnf  32855  disjorf  32864  disjunsn  32879  ac6sf2  32907  nn0min  33105  tosglblem  33234  archiabl  33458  1arithidom  33771  eulerpartlems  34694  eulerpartlemr  34708  eulerpartlemn  34715  ballotlem7  34870  bnj110  35190  bnj92  35194  bnj539  35223  bnj540  35224  bnj580  35245  bnj978  35281  bnj1047  35305  bnj1128  35322  bnj1417  35373  bnj1421  35374  bnj1312  35390  bnj1498  35393  onvf1od  35489  lfuhgr3  35510  subfacp1lem3  35572  cvmlift2lem1  35692  cvmlift2lem12  35704  satfv1  35753  fmlaomn0  35780  fmla0disjsuc  35788  fmlasucdisj  35789  untuni  36099  dfso3  36110  elintfv  36155  elpotr  36169  dfon2lem7  36177  dfon2lem9  36179  dfint3  36342  brlb  36345  filnetlem4  36780  axtco  36870  axtco1g  36875  regsfromregtco  36937  mh-infprim3bi  36947  bj-reabeq  37550  bj-axseprep  37598  ctbssinf  37939  fvineqsneq  37945  pibt2  37950  phpreu  38142  ptrecube  38158  poimirlem1  38159  poimirlem25  38183  poimirlem26  38184  poimirlem27  38185  poimirlem30  38188  mblfinlem2  38196  ftc1anc  38239  inixp  38266  ac6gf  38270  heibor1lem  38347  heiborlem1  38349  iscrngo2  38535  ac6s3f  38709  ref5  38857  idinxpssinxp2  38862  n0elqs  38870  ineleq  38892  ralrnmo  38899  ssdmral  38917  refrelcosslem  39090  refrelcoss3  39091  lpssat  39676  lssat  39679  lcvbr2  39685  lcvbr3  39686  lfl1  39733  lub0N  39852  glb0N  39856  atlrelat1  39984  hlrelat2  40066  ispsubsp2  40409  pclclN  40554  cdleme25cv  41021  tendoeq2  41437  cdlemk35  41575  aks4d1p7  42739  sticksstones1  42802  indstrd  42849  supinf  42899  infdesc  43266  setindtrs  43643  unielss  43836  ssunib  43838  onsupmaxb  43857  onsupeqnmax  43865  cllem0  44183  ntrneixb  44712  gneispace  44751  expandral  44891  ismnuprim  44895  dfuniv2  44903  undisjrab  44907  zfregs2VD  45440  sswfaxreg  45587  dfac5prim  45590  permac8prim  45614  iindif2f  45769  ralfal  45770  disjinfi  45801  iuneqfzuz  45942  caucvgbf  46094  rexanuz2nf  46097  mccl  46205  limsupub  46309  limsuppnflem  46315  limsupre2lem  46329  lmbr3v  46350  liminfpnfuz  46421  xlimpnfxnegmnf2  46463  ioodvbdlimc1lem2  46537  ioodvbdlimc2lem  46539  dvnprodlem3  46553  fourierdlem103  46814  fourierdlem104  46815  sge0iunmpt  47023  meaiuninc3v  47089  hoidmvle  47205  issmff  47339  n0nsn2el  47650  r19.32  47723  2rexrsb  47727  cbvral2  47728  2reu3  47735  2reu8i  47738  otiunsndisjX  47904  0nelsetpreimafv  48027  dfgric2  48568  gpg5nbgrvtx03starlem1  48721  gpg5nbgrvtx03starlem2  48722  gpg5nbgrvtx03starlem3  48723  gpg5nbgrvtx13starlem1  48724  gpg5nbgrvtx13starlem2  48725  gpg5nbgrvtx13starlem3  48726  gpg5edgnedg  48783  copisnmnd  48822  lindslinindsimp1  49121  lindslinindsimp2  49127  snlindsntor  49135  ldepslinc  49173  iuneq0  49481  iinxp  49493  iscnrm3  49614  setrec1lem3  50351  ralsbii  50463  aacllem  50474