Theorem ralbii 3113

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

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

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

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

This theorem is used by:  dfral2  3118  ralinexa  3120  rexanali  3121  r19.26-3  3128  ralbiim  3129  2ralbii  3142  3ralbii  3144  4ralbii  3145  2ralbiim  3146  ralnex2  3147  nrexralim  3151  r19.26-2  3152  r19.23v  3194  r19.32v  3200  2ralor  3241  nelb  3243  cbvral2vw  3249  cbvral3vw  3251  ralrot3  3298  ralcom13  3299  sbralieALT  3345  cbvral2v  3359  cbvral3v  3361  ceqsralv  3497  ralxpxfr2d  3607  reu8  3698  2reuswap  3711  2reu5lem2  3721  2rmoswap  3726  rmoanim  3849  rmoanimALT  3850  dfdif3  4073  dfss5  4228  n0el  4319  ralnralall  4476  2reu4lem  4486  r19.12sn  4688  raldifsnb  4766  eqsn  4797  n0snor2el  4800  uni0b  4901  uni0c  4902  ssint  4931  iuniin  4971  iuneq2  4978  iunssf  5009  iunssfOLD  5010  iunss  5011  iunssOLD  5012  ssiinf  5021  iinab  5034  iinun2  5039  iindif1  5043  iindif2  5045  iinin2  5046  iinuni  5066  sspwuni  5068  iinpw  5074  disjor  5093  disjxun  5109  dftr3  5225  reusv3  5378  otiunsndisj  5505  ssrel2  5773  reliun  5805  xpiindi  5823  rexiunxp  5828  ralxpf  5834  rexxpf  5835  dfse2  6104  idrefALT  6115  asymref2  6119  rninxp  6179  dminxp  6180  cnviin  6291  cnvpo  6292  dfpo2  6301  dfse3  6341  frpoins2fg  6349  dffun9  6569  funcnv3  6610  fncnv  6613  fnres  6666  mptfnf  6674  fnopabg  6676  mptfng  6678  fint  6761  funimass4  6949  fndmdifeq0  7043  funconstss  7055  f1ompt  7110  idref  7148  fconstfv  7217  dff13f  7258  dff14b  7274  weniso  7363  fnssintima  7371  foov  7594  imaeqalov  7659  dfwe2  7779  tfis2f  7858  tfindes  7865  frxp  8128  ralxp3f  8139  frpoins3xpg  8142  frpoins3xp3g  8143  xpord2indlem  8149  xpord3inddlem  8156  soseq  8161  tz7.48lem  8434  tz7.49  8438  oeordi  8579  naddcllem  8668  naddunif  8686  naddasslem2  8688  ixpeq2  8915  ixpin  8927  ixpiin  8928  boxriin  8944  findcard3  9250  fimax2g  9253  fissuni  9321  indexfi  9324  dfsup2  9411  sup0riota  9433  infcllem  9455  wemapsolem  9519  zfinf2  9618  oemapso  9658  ttrclresv  9693  zfregs2  9709  setinds  9725  setinds2f  9726  frins2f  9732  r1elss  9785  rankc1  9849  cp  9890  bnd2  9892  aceq1  10117  aceq2  10119  kmlem7  10156  kmlem12  10161  kmlem13  10162  kmlem15  10164  fin12  10412  ac6num  10478  ac6s2  10485  ac6sf  10488  ac6s4  10489  zorn2lem4  10498  zorn2lem6  10500  zorn2lem7  10501  zorng  10503  ttukeylem6  10513  brdom7disj  10530  brdom6disj  10531  fpwwe2  10645  fpwwe  10648  axgroth5  10826  axgroth4  10834  grothprim  10836  nqereu  10931  dfinfre  12213  infrenegsup  12215  xrsupsslem  13351  xrinfmsslem  13352  xrinfmss2  13355  fzshftral  13662  fsuppmapnn0ub  14051  mptnn0fsuppr  14055  hashgt12el  14479  hashgt12el2  14480  hashbc  14510  s3iunsndisj  15031  cotr2g  15039  rexfiuz  15425  clim0  15583  rpnnen2lem12  16305  gcdcllem1  16581  absproddvds  16699  coprmproddvdslem  16744  vdwmc2  17063  vdwlem13  17077  vdwnn  17082  xpscf  17643  mreacs  17738  acsfn  17739  acsfn1  17741  acsfn2  17743  dfinito2  18084  dftermo2  18085  ispos2  18395  lublecllem  18438  odulub  18485  oduglb  18487  posglbdg  18493  isnmnd  18830  gsumwspan  18944  smndex2dnrinv  19016  isnsg2  19268  oppgid  19472  oppgcntz  19480  efgval2  19840  iscyggen2  19997  iscyg3  20002  oppr1  20480  isnirred  20550  isdomn5  20861  lssne0  21124  iunocv  21883  islindf4  22040  pmatcollpw2lem  22986  isbasis2g  23157  basdif0  23162  tgval2  23165  ntreq0  23286  isclo2  23297  opnnei  23329  neiptopnei  23341  lmres  23509  ist1-3  23558  cmpcov2  23599  cmpsub  23609  is1stc2  23651  1stccn  23673  kgencn  23766  eltx  23778  txkgen  23862  fbun  24050  trfbas  24054  fbunfip  24079  trfil2  24097  isufil2  24118  fixufil  24132  hausflim  24191  txflf  24216  fclsopn  24224  alexsubALTlem3  24259  isclmp  25309  iscau3  25490  iscau4  25491  caucfil  25495  bcth3  25543  ovolgelb  25692  dyadmax  25810  itg2leub  25946  itg2cn  25975  plydivex  26511  vieta1  26526  lgseisenlem2  27593  pnt3  27829  nosepon  27882  nomaxmo  27915  nosupbnd1lem4  27928  conway  28025  eqcuts2  28032  etaslts  28039  lesrec  28045  bday1  28060  cuteq1  28063  madebdaylemlrcut  28145  addsproplem4  28218  addsproplem6  28220  addsprop  28222  addsuniflem  28247  mulsuniflem  28395  oncutlt  28510  oniso  28517  onsfi  28602  bdayn0p1  28615  addhalfcut  28705  tglowdim2ln  28978  axcontlem12  29382  elntg2  29392  numedglnl  29551  lfuhgr3  29557  vtxd0nedgb  29898  wlkvtxedg  30053  pthd  30184  2pthdlem1  30348  clwlkclwwlk  30422  3pthdlem1  30588  frgrregord013  30819  grpoidinvlem3  30931  nmoubi  31197  lnon0  31223  adjsym  32258  nmopub  32333  nmfnleub  32350  cvbr2  32708  chpssati  32788  chrelat2i  32790  chrelat3  32796  mdsymlem8  32835  ralcom4f  32887  reuxfrdf  32910  n0nsnel  32934  uniinn0  32970  ssiun3  32976  disjnf  32988  disjorf  32997  disjunsn  33012  ac6sf2  33040  nn0min  33237  tosglblem  33360  archiabl  33584  1arithidom  33893  eulerpartlems  34817  eulerpartlemr  34831  eulerpartlemn  34838  ballotlem7  34993  bnj110  35313  bnj92  35317  bnj539  35346  bnj540  35347  bnj580  35368  bnj978  35404  bnj1047  35428  bnj1128  35445  bnj1417  35496  bnj1421  35497  bnj1312  35513  bnj1498  35516  onvf1od  35650  subfacp1lem3  35713  cvmlift2lem1  35833  cvmlift2lem12  35845  satfv1  35894  fmlaomn0  35921  fmla0disjsuc  35929  fmlasucdisj  35930  untuni  36240  dfso3  36251  elintfv  36296  elpotr  36310  dfon2lem7  36318  dfon2lem9  36320  dfint3  36483  brlb  36486  filnetlem4  36951  axtco  37041  axtco1g  37046  regsfromregtco  37108  mh-infprim3bi  37118  bj-reabeq  37722  bj-axseprep  37770  ctbssinf  38111  fvineqsneq  38117  pibt2  38122  phpreu  38314  ptrecube  38330  poimirlem1  38331  poimirlem25  38355  poimirlem26  38356  poimirlem27  38357  poimirlem30  38360  mblfinlem2  38368  ftc1anc  38411  inixp  38439  ac6gf  38443  heibor1lem  38520  heiborlem1  38522  iscrngo2  38708  ac6s3f  38880  ref5  39028  idinxpssinxp2  39033  n0elqs  39041  ineleq  39063  ralrnmo  39070  ssdmral  39088  refrelcosslem  39261  refrelcoss3  39262  lpssat  39847  lssat  39850  lcvbr2  39856  lcvbr3  39857  lfl1  39904  lub0N  40023  glb0N  40027  atlrelat1  40155  hlrelat2  40237  ispsubsp2  40580  pclclN  40725  cdleme25cv  41192  tendoeq2  41608  cdlemk35  41746  aks4d1p7  42910  sticksstones1  42973  indstrd  43020  supinf  43070  infdesc  43435  setindtrs  43812  unielss  44005  ssunib  44007  onsupmaxb  44026  onsupeqnmax  44034  cllem0  44352  ntrneixb  44881  gneispace  44920  expandral  45060  ismnuprim  45064  dfuniv2  45072  undisjrab  45076  zfregs2VD  45609  sswfaxreg  45756  dfac5prim  45759  permac8prim  45783  iindif2f  45938  ralfal  45939  disjinfi  45970  iuneqfzuz  46111  caucvgbf  46263  rexanuz2nf  46266  mccl  46374  limsupub  46478  limsuppnflem  46484  limsupre2lem  46498  lmbr3v  46519  liminfpnfuz  46590  xlimpnfxnegmnf2  46632  ioodvbdlimc1lem2  46706  ioodvbdlimc2lem  46708  dvnprodlem3  46722  fourierdlem103  46983  fourierdlem104  46984  sge0iunmpt  47192  meaiuninc3v  47258  hoidmvle  47374  issmff  47508  n0nsn2el  47822  r19.32  47895  2rexrsb  47899  cbvral2  47900  2reu3  47907  2reu8i  47910  otiunsndisjX  48076  0nelsetpreimafv  48199  dfgric2  48740  gpg5nbgrvtx03starlem1  48893  gpg5nbgrvtx03starlem2  48894  gpg5nbgrvtx03starlem3  48895  gpg5nbgrvtx13starlem1  48896  gpg5nbgrvtx13starlem2  48897  gpg5nbgrvtx13starlem3  48898  gpg5edgnedg  48955  copisnmnd  48993  lindslinindsimp1  49296  lindslinindsimp2  49302  snlindsntor  49310  ldepslinc  49348  iuneq0  49656  iinxp  49668  iscnrm3  49789  setrec1lem3  50526  ralsbii  50638  ralseubii  50670  aacllem  50680