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  7773  tfis2f  7852  tfindes  7859  frxp  8122  ralxp3f  8133  frpoins3xpg  8136  frpoins3xp3g  8137  xpord2indlem  8143  xpord3inddlem  8150  soseq  8155  tz7.48lem  8428  tz7.49  8432  oeordi  8573  naddcllem  8662  naddunif  8680  naddasslem2  8682  ixpeq2  8909  ixpin  8921  ixpiin  8922  boxriin  8938  findcard3  9243  fimax2g  9246  fissuni  9314  indexfi  9317  dfsup2  9404  sup0riota  9426  infcllem  9448  wemapsolem  9512  zfinf2  9611  oemapso  9651  ttrclresv  9686  zfregs2  9702  setinds  9718  setinds2f  9719  frins2f  9725  r1elss  9778  rankc1  9842  cp  9877  bnd2  9879  aceq1  10101  aceq2  10103  kmlem7  10140  kmlem12  10145  kmlem13  10146  kmlem15  10148  fin12  10397  ac6num  10463  ac6s2  10470  ac6sf  10473  ac6s4  10474  zorn2lem4  10483  zorn2lem6  10485  zorn2lem7  10486  zorng  10488  ttukeylem6  10498  brdom7disj  10515  brdom6disj  10516  fpwwe2  10628  fpwwe  10631  axgroth5  10809  axgroth4  10817  grothprim  10819  nqereu  10914  dfinfre  12196  infrenegsup  12198  xrsupsslem  13333  xrinfmsslem  13334  xrinfmss2  13337  fzshftral  13643  fsuppmapnn0ub  14031  mptnn0fsuppr  14035  hashgt12el  14459  hashgt12el2  14460  hashbc  14490  s3iunsndisj  15005  cotr2g  15013  rexfiuz  15399  clim0  15557  rpnnen2lem12  16281  gcdcllem1  16557  absproddvds  16675  coprmproddvdslem  16720  vdwmc2  17039  vdwlem13  17053  vdwnn  17058  xpscf  17619  mreacs  17714  acsfn  17715  acsfn1  17717  acsfn2  17719  dfinito2  18060  dftermo2  18061  ispos2  18371  lublecllem  18414  odulub  18461  oduglb  18463  posglbdg  18469  isnmnd  18796  gsumwspan  18905  smndex2dnrinv  18977  isnsg2  19222  oppgid  19426  oppgcntz  19434  efgval2  19794  iscyggen2  19951  iscyg3  19956  oppr1  20432  isnirred  20502  isdomn5  20795  lssne0  21050  iunocv  21800  islindf4  21957  pmatcollpw2lem  22903  isbasis2g  23074  basdif0  23079  tgval2  23082  ntreq0  23203  isclo2  23214  opnnei  23246  neiptopnei  23258  lmres  23426  ist1-3  23475  cmpcov2  23516  cmpsub  23526  is1stc2  23568  1stccn  23589  kgencn  23682  eltx  23694  txkgen  23778  fbun  23966  trfbas  23970  fbunfip  23995  trfil2  24013  isufil2  24034  fixufil  24048  hausflim  24107  txflf  24132  fclsopn  24140  alexsubALTlem3  24175  isclmp  25225  iscau3  25406  iscau4  25407  caucfil  25411  bcth3  25459  ovolgelb  25608  dyadmax  25726  itg2leub  25862  itg2cn  25891  plydivex  26427  vieta1  26442  lgseisenlem2  27506  pnt3  27742  nosepon  27795  nomaxmo  27828  nosupbnd1lem4  27841  conway  27938  eqcuts2  27945  etaslts  27952  lesrec  27958  bday1  27973  cuteq1  27976  madebdaylemlrcut  28058  addsproplem4  28131  addsproplem6  28133  addsprop  28135  addsuniflem  28160  mulsuniflem  28308  oncutlt  28423  oniso  28430  onsfi  28515  bdayn0p1  28528  addhalfcut  28618  tglowdim2ln  28887  axcontlem12  29266  elntg2  29276  numedglnl  29435  vtxd0nedgb  29779  wlkvtxedg  29934  pthd  30059  2pthdlem1  30220  clwlkclwwlk  30294  3pthdlem1  30456  frgrregord013  30687  grpoidinvlem3  30799  nmoubi  31065  lnon0  31091  adjsym  32126  nmopub  32201  nmfnleub  32218  cvbr2  32576  chpssati  32656  chrelat2i  32658  chrelat3  32664  mdsymlem8  32703  ralcom4f  32755  reuxfrdf  32778  n0nsnel  32802  uniinn0  32838  ssiun3  32844  disjnf  32856  disjorf  32865  disjunsn  32880  ac6sf2  32908  nn0min  33106  tosglblem  33235  archiabl  33459  1arithidom  33772  eulerpartlems  34695  eulerpartlemr  34709  eulerpartlemn  34716  ballotlem7  34871  bnj110  35191  bnj92  35195  bnj539  35224  bnj540  35225  bnj580  35246  bnj978  35282  bnj1047  35306  bnj1128  35323  bnj1417  35374  bnj1421  35375  bnj1312  35391  bnj1498  35394  onvf1od  35490  lfuhgr3  35511  subfacp1lem3  35573  cvmlift2lem1  35693  cvmlift2lem12  35705  satfv1  35754  fmlaomn0  35781  fmla0disjsuc  35789  fmlasucdisj  35790  untuni  36100  dfso3  36111  elintfv  36156  elpotr  36170  dfon2lem7  36178  dfon2lem9  36180  dfint3  36343  brlb  36346  filnetlem4  36781  axtco  36871  axtco1g  36876  regsfromregtco  36938  mh-infprim3bi  36948  bj-reabeq  37551  bj-axseprep  37599  ctbssinf  37940  fvineqsneq  37946  pibt2  37951  phpreu  38143  ptrecube  38159  poimirlem1  38160  poimirlem25  38184  poimirlem26  38185  poimirlem27  38186  poimirlem30  38189  mblfinlem2  38197  ftc1anc  38240  inixp  38267  ac6gf  38271  heibor1lem  38348  heiborlem1  38350  iscrngo2  38536  ac6s3f  38710  ref5  38858  idinxpssinxp2  38863  n0elqs  38871  ineleq  38893  ralrnmo  38900  ssdmral  38918  refrelcosslem  39091  refrelcoss3  39092  lpssat  39677  lssat  39680  lcvbr2  39686  lcvbr3  39687  lfl1  39734  lub0N  39853  glb0N  39857  atlrelat1  39985  hlrelat2  40067  ispsubsp2  40410  pclclN  40555  cdleme25cv  41022  tendoeq2  41438  cdlemk35  41576  aks4d1p7  42740  sticksstones1  42803  indstrd  42850  supinf  42900  infdesc  43267  setindtrs  43644  unielss  43837  ssunib  43839  onsupmaxb  43858  onsupeqnmax  43866  cllem0  44184  ntrneixb  44713  gneispace  44752  expandral  44892  ismnuprim  44896  dfuniv2  44904  undisjrab  44908  zfregs2VD  45441  sswfaxreg  45588  dfac5prim  45591  permac8prim  45615  iindif2f  45770  ralfal  45771  disjinfi  45802  iuneqfzuz  45943  caucvgbf  46095  rexanuz2nf  46098  mccl  46206  limsupub  46310  limsuppnflem  46316  limsupre2lem  46330  lmbr3v  46351  liminfpnfuz  46422  xlimpnfxnegmnf2  46464  ioodvbdlimc1lem2  46538  ioodvbdlimc2lem  46540  dvnprodlem3  46554  fourierdlem103  46815  fourierdlem104  46816  sge0iunmpt  47024  meaiuninc3v  47090  hoidmvle  47206  issmff  47340  n0nsn2el  47651  r19.32  47724  2rexrsb  47728  cbvral2  47729  2reu3  47736  2reu8i  47739  otiunsndisjX  47905  0nelsetpreimafv  48028  dfgric2  48569  gpg5nbgrvtx03starlem1  48722  gpg5nbgrvtx03starlem2  48723  gpg5nbgrvtx03starlem3  48724  gpg5nbgrvtx13starlem1  48725  gpg5nbgrvtx13starlem2  48726  gpg5nbgrvtx13starlem3  48727  gpg5edgnedg  48784  copisnmnd  48823  lindslinindsimp1  49122  lindslinindsimp2  49128  snlindsntor  49136  ldepslinc  49174  iuneq0  49482  iinxp  49494  iscnrm3  49615  setrec1lem3  50352  ralsbii  50464  aacllem  50475