Theorem ralbii 3108

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

Syntax hints:   ↔ wb 208   ∈ wcel 2142  ∀wral 3076

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

This theorem depends on definitions:  df-bi 209  df-ral 3077

This theorem is referenced by:  dfral2  3113  ralinexa  3115  rexanali  3116  r19.26-3  3123  ralbiim  3124  2ralbii  3137  3ralbii  3139  4ralbii  3140  2ralbiim  3141  ralnex2  3142  nrexralim  3146  r19.26-2  3147  r19.23v  3189  r19.32v  3195  2ralor  3236  nelb  3238  cbvral2vw  3244  cbvral3vw  3246  ralrot3  3293  ralcom13  3294  sbralieALT  3341  cbvral2v  3355  cbvral3v  3357  ceqsralv  3494  ralxpxfr2d  3605  reu8  3696  2reuswap  3709  2reu5lem2  3719  2rmoswap  3724  rmoanim  3847  rmoanimALT  3848  dfdif3  4071  dfss5  4227  n0el  4317  ralnralall  4467  2reu4lem  4477  r19.12sn  4679  raldifsnb  4756  eqsn  4787  n0snor2el  4791  uni0b  4892  uni0c  4893  ssint  4922  iuniin  4962  iuneq2  4969  iunssf  5000  iunssfOLD  5001  iunss  5002  iunssOLD  5003  ssiinf  5012  iinab  5025  iinun2  5030  iindif1  5032  iindif2  5034  iinin2  5035  iinuni  5055  sspwuni  5057  iinpw  5063  disjor  5082  disjxun  5098  dftr3  5212  reusv3  5362  otiunsndisj  5489  ssrel2  5757  reliun  5789  xpiindi  5807  rexiunxp  5812  ralxpf  5818  rexxpf  5819  dfse2  6089  idrefALT  6100  asymref2  6104  rninxp  6165  dminxp  6166  cnviin  6273  cnvpo  6274  dfpo2  6283  dfse3  6323  frpoins2fg  6331  dffun9  6550  funcnv3  6591  fncnv  6594  fnres  6648  mptfnf  6656  fnopabg  6658  mptfng  6660  fint  6743  funimass4  6931  fndmdifeq0  7025  funconstss  7037  f1ompt  7092  idref  7128  fconstfv  7196  dff13f  7239  dff14b  7255  weniso  7338  fnssintima  7346  foov  7570  imaeqalov  7635  dfwe2  7757  tfis2f  7836  tfindes  7843  frxp  8106  ralxp3f  8117  frpoins3xpg  8120  frpoins3xp3g  8121  xpord2indlem  8127  xpord3inddlem  8134  soseq  8139  tz7.48lem  8412  tz7.49  8416  oeordi  8557  naddcllem  8646  naddunif  8664  naddasslem2  8666  ixpeq2  8893  ixpin  8905  ixpiin  8906  boxriin  8922  findcard3  9227  fimax2g  9230  fissuni  9300  indexfi  9303  dfsup2  9390  sup0riota  9412  infcllem  9434  wemapsolem  9498  zfinf2  9597  oemapso  9637  ttrclresv  9672  zfregs2  9688  setinds  9704  setinds2f  9705  frins2f  9711  r1elss  9764  rankc1  9828  cp  9849  bnd2  9851  aceq1  10073  aceq2  10075  kmlem7  10113  kmlem12  10118  kmlem13  10119  kmlem15  10121  fin12  10370  ac6num  10436  ac6s2  10443  ac6sf  10446  ac6s4  10447  zorn2lem4  10456  zorn2lem6  10458  zorn2lem7  10459  zorng  10461  ttukeylem6  10471  brdom7disj  10488  brdom6disj  10489  fpwwe2  10601  fpwwe  10604  axgroth5  10782  axgroth4  10790  grothprim  10792  nqereu  10887  dfinfre  12173  infrenegsup  12175  xrsupsslem  13310  xrinfmsslem  13311  xrinfmss2  13314  fzshftral  13620  fsuppmapnn0ub  14008  mptnn0fsuppr  14012  hashgt12el  14435  hashgt12el2  14436  hashbc  14466  s3iunsndisj  14981  cotr2g  14989  rexfiuz  15375  clim0  15533  rpnnen2lem12  16257  gcdcllem1  16533  absproddvds  16651  coprmproddvdslem  16696  vdwmc2  17015  vdwlem13  17029  vdwnn  17034  xpscf  17595  mreacs  17690  acsfn  17691  acsfn1  17693  acsfn2  17695  dfinito2  18036  dftermo2  18037  ispos2  18347  lublecllem  18390  odulub  18437  oduglb  18439  posglbdg  18445  isnmnd  18772  gsumwspan  18880  smndex2dnrinv  18952  isnsg2  19197  oppgid  19396  oppgcntz  19404  efgval2  19764  iscyggen2  19921  iscyg3  19926  oppr1  20399  isnirred  20469  isdomn5  20760  isdomn2OLD  20762  lssne0  21018  iunocv  21733  islindf4  21890  pmatcollpw2lem  22837  isbasis2g  23008  basdif0  23013  tgval2  23016  ntreq0  23137  isclo2  23148  opnnei  23180  neiptopnei  23192  lmres  23360  ist1-3  23409  cmpcov2  23450  cmpsub  23460  is1stc2  23502  1stccn  23523  kgencn  23616  eltx  23628  txkgen  23712  fbun  23900  trfbas  23904  fbunfip  23929  trfil2  23947  isufil2  23968  fixufil  23982  hausflim  24041  txflf  24066  fclsopn  24074  alexsubALTlem3  24109  isclmp  25159  iscau3  25340  iscau4  25341  caucfil  25345  bcth3  25393  ovolgelb  25542  dyadmax  25660  itg2leub  25796  itg2cn  25825  plydivex  26361  vieta1  26376  lgseisenlem2  27440  pnt3  27676  nosepon  27729  nomaxmo  27762  nosupbnd1lem4  27775  conway  27872  eqcuts2  27879  etaslts  27886  lesrec  27892  bday1  27907  cuteq1  27910  madebdaylemlrcut  27992  addsproplem4  28065  addsproplem6  28067  addsprop  28069  addsuniflem  28094  mulsuniflem  28242  oncutlt  28357  oniso  28364  onsfi  28449  bdayn0p1  28462  addhalfcut  28552  tglowdim2ln  28821  axcontlem12  29176  elntg2  29186  numedglnl  29345  vtxd0nedgb  29689  wlkvtxedg  29844  pthd  29969  2pthdlem1  30130  clwlkclwwlk  30204  3pthdlem1  30366  frgrregord013  30597  grpoidinvlem3  30709  nmoubi  30975  lnon0  31001  adjsym  32036  nmopub  32111  nmfnleub  32128  cvbr2  32486  chpssati  32566  chrelat2i  32568  chrelat3  32574  mdsymlem8  32613  ralcom4f  32667  reuxfrdf  32690  n0nsnel  32714  uniinn0  32750  ssiun3  32758  disjnf  32770  disjorf  32779  disjunsn  32794  ac6sf2  32824  nn0min  33023  tosglblem  33152  archiabl  33378  1arithidom  33733  eulerpartlems  34657  eulerpartlemr  34671  eulerpartlemn  34678  ballotlem7  34833  bnj110  35153  bnj92  35157  bnj539  35186  bnj540  35187  bnj580  35208  bnj978  35244  bnj1047  35268  bnj1128  35285  bnj1417  35336  bnj1421  35337  bnj1312  35353  bnj1498  35356  onvf1od  35450  lfuhgr3  35470  subfacp1lem3  35532  cvmlift2lem1  35652  cvmlift2lem12  35664  satfv1  35713  fmlaomn0  35740  fmla0disjsuc  35748  fmlasucdisj  35749  untuni  36059  dfso3  36070  elintfv  36115  elpotr  36129  dfon2lem7  36137  dfon2lem9  36139  dfint3  36302  brlb  36305  filnetlem4  36741  axtco  36831  axtco1g  36836  regsfromregtco  36898  mh-infprim3bi  36908  bj-reabeq  37512  bj-axseprep  37559  ctbssinf  37900  fvineqsneq  37906  pibt2  37911  phpreu  38103  ptrecube  38119  poimirlem1  38120  poimirlem25  38144  poimirlem26  38145  poimirlem27  38146  poimirlem30  38149  mblfinlem2  38157  ftc1anc  38200  inixp  38227  ac6gf  38231  heibor1lem  38308  heiborlem1  38310  iscrngo2  38496  ac6s3f  38670  ref5  38818  idinxpssinxp2  38823  n0elqs  38831  ineleq  38853  ralrnmo  38860  ssdmral  38878  refrelcosslem  39051  refrelcoss3  39052  lpssat  39637  lssat  39640  lcvbr2  39646  lcvbr3  39647  lfl1  39694  lub0N  39813  glb0N  39817  atlrelat1  39945  hlrelat2  40027  ispsubsp2  40370  pclclN  40515  cdleme25cv  40982  tendoeq2  41398  cdlemk35  41536  aks4d1p7  42700  sticksstones1  42763  indstrd  42810  supinf  42858  infdesc  43225  setindtrs  43602  unielss  43795  ssunib  43797  onsupmaxb  43816  onsupeqnmax  43824  cllem0  44142  ntrneixb  44671  gneispace  44710  expandral  44866  ismnuprim  44870  dfuniv2  44878  undisjrab  44882  zfregs2VD  45416  sswfaxreg  45563  dfac5prim  45566  permac8prim  45590  iindif2f  45738  ralfal  45739  disjinfi  45770  iuneqfzuz  45911  caucvgbf  46063  rexanuz2nf  46066  mccl  46174  limsupub  46278  limsuppnflem  46284  limsupre2lem  46298  lmbr3v  46319  liminfpnfuz  46390  xlimpnfxnegmnf2  46432  ioodvbdlimc1lem2  46506  ioodvbdlimc2lem  46508  dvnprodlem3  46522  fourierdlem103  46783  fourierdlem104  46784  sge0iunmpt  46992  meaiuninc3v  47058  hoidmvle  47174  issmff  47308  n0nsn2el  47619  r19.32  47692  2rexrsb  47696  cbvral2  47697  2reu3  47704  2reu8i  47707  otiunsndisjX  47873  0nelsetpreimafv  47996  dfgric2  48537  gpg5nbgrvtx03starlem1  48690  gpg5nbgrvtx03starlem2  48691  gpg5nbgrvtx03starlem3  48692  gpg5nbgrvtx13starlem1  48693  gpg5nbgrvtx13starlem2  48694  gpg5nbgrvtx13starlem3  48695  gpg5edgnedg  48752  copisnmnd  48791  lindslinindsimp1  49079  lindslinindsimp2  49085  snlindsntor  49093  ldepslinc  49131  iuneq0  49440  iinxp  49452  iscnrm3  49573  setrec1lem3  50310  aacllem  50422