Theorem ralbii 3112

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2147  ∀wral 3080

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 3081

This theorem is used by:  dfral2  3117  ralinexa  3119  rexanali  3120  r19.26-3  3127  ralbiim  3128  2ralbii  3141  3ralbii  3143  4ralbii  3144  2ralbiim  3145  ralnex2  3146  nrexralim  3150  r19.26-2  3151  r19.23v  3193  r19.32v  3199  2ralor  3240  nelb  3242  cbvral2vw  3248  cbvral3vw  3250  ralrot3  3297  ralcom13  3298  sbralieALT  3343  cbvral2v  3357  cbvral3v  3359  ceqsralv  3494  ralxpxfr2d  3603  reu8  3694  2reuswap  3707  2reu5lem2  3717  2rmoswap  3722  rmoanim  3846  rmoanimALT  3847  dfdif3  4058  dfss5  4223  n0el  4315  ralnralall  4472  2reu4lem  4482  r19.12sn  4683  raldifsnb  4761  eqsn  4790  n0snor2el  4793  uni0b  4899  uni0c  4900  ssint  4929  iuniin  4969  iuneq2  4976  iunssf  5006  iunssfOLD  5007  iunss  5008  iunssOLD  5009  ssiinf  5018  iinab  5031  iinun2  5036  iindif1  5040  iindif2  5042  iinin2  5043  iinuni  5063  sspwuni  5065  iinpw  5071  disjor  5090  disjxun  5106  dftr3  5223  reusv3  5374  otiunsndisj  5500  ssrel2  5770  reliun  5803  xpiindi  5822  rexiunxp  5827  ralxpf  5834  rexxpf  5835  dfse2  6116  idrefALT  6125  asymref2  6129  rninxp  6189  dminxp  6190  cnviin  6313  cnvpo  6314  dfpo2  6325  dfse3  6365  frpoins2fg  6373  dffun9  6597  funcnv3  6640  fncnv  6643  fnres  6696  mptfnf  6704  fnopabg  6706  mptfng  6708  fint  6791  funimass4  6980  fndmdifeq0  7074  funconstss  7086  f1ompt  7143  idref  7181  fconstfv  7249  dff13f  7290  dff14b  7306  weniso  7395  fnssintima  7403  foov  7627  imaeqalov  7692  dfwe2  7820  tfis2f  7901  tfindes  7908  ovmptss  8139  frxp  8175  ralxp3f  8191  frpoins3xpg  8194  frpoins3xp3g  8195  xpord2indlem  8201  xpord3inddlem  8208  soseq  8213  tz7.48lemOLD  8489  tz7.49  8493  oeordi  8634  naddcllem  8723  naddunif  8741  naddasslem2  8743  ixpeq2  8977  ixpin  8989  ixpiin  8990  boxriin  9006  findcard3  9312  fimax2g  9315  fissuni  9384  indexfi  9387  dfsup2  9473  sup0riota  9495  infcllem  9517  wemapsolem  9581  zfinf2  9680  oemapso  9720  ttrclresv  9755  zfregs2  9771  setinds  9787  setinds2f  9788  frins2f  9794  r1elss  9851  rankc1  9924  elhf4  9949  cp  9991  bnd2  9993  setrec1lem3  10006  aceq1  10235  aceq2  10237  kmlem7  10274  kmlem12  10279  kmlem13  10280  kmlem15  10282  fin12  10530  ac6num  10596  ac6s2  10603  ac6sf  10606  ac6s4  10607  zorn2lem4  10616  zorn2lem6  10618  zorn2lem7  10619  zorng  10621  ttukeylem6  10631  brdom7disj  10649  brdom6disj  10650  fpwwe2  10767  fpwwe  10770  axgroth5  10948  axgroth4  10956  grothprim  10958  nqereu  11053  dfinfre  12338  infrenegsup  12340  xrsupsslem  13477  xrinfmsslem  13478  xrinfmss2  13481  fzshftral  13789  fsuppmapnn0ub  14178  mptnn0fsuppr  14182  hashgt12el  14608  hashgt12el2  14609  hashbc  14639  s3iunsndisj  15164  cotr2g  15172  rexfiuz  15559  clim0  15717  rpnnen2lem12  16437  gcdcllem1  16713  absproddvds  16836  coprmproddvdslem  16881  vdwmc2  17201  vdwlem13  17215  vdwnn  17220  xpscf  17787  mreacs  17882  acsfn  17883  acsfn1  17885  acsfn2  17887  dfinito2  18228  dftermo2  18229  ispos2  18539  lublecllem  18582  odulub  18629  oduglb  18631  posglbdg  18637  isnmnd  18977  gsumwspan  19092  smndex2dnrinv  19164  isnsg2  19416  oppgid  19621  oppgcntz  19629  efgval2  19989  iscyggen2  20146  iscyg3  20151  dfring3  20569  oppr1  20631  isnirred  20701  isdomn5  21013  lssne0  21277  iunocv  22042  islindf4  22199  pmatcollpw2lem  23150  isbasis2g  23321  basdif0  23326  tgval2  23329  ntreq0  23450  isclo2  23461  opnnei  23493  neiptopnei  23505  lmres  23673  ist1-3  23722  cmpcov2  23763  cmpsub  23773  is1stc2  23815  1stccn  23837  kgencn  23930  eltx  23942  txkgen  24026  fbun  24214  trfbas  24218  fbunfip  24243  trfil2  24261  isufil2  24282  fixufil  24296  hausflim  24355  txflf  24380  fclsopn  24388  alexsubALTlem3  24423  isclmp  25473  iscau3  25654  iscau4  25655  caucfil  25659  bcth3  25707  ovolgelb  25856  dyadmax  25974  itg2leub  26110  itg2cn  26139  plydivex  26673  vieta1  26690  lgseisenlem2  27760  pnt3  27996  infdesc  28024  nosepon  28079  nomaxmo  28112  nosupbnd1lem4  28125  conway  28222  eqcuts2  28229  etaslts  28236  lesrec  28242  bday1  28257  cuteq1  28260  madebdaylemlrcut  28342  addsproplem4  28415  addsproplem6  28417  addsprop  28419  addsuniflem  28444  mulsuniflem  28592  oncutlt  28707  oniso  28714  onsfi  28799  bdayn0p1  28812  addhalfcut  28902  tglowdim2ln  29177  axcontlem12  29610  elntg2  29620  numedglnl  29779  lfuhgr3  29785  vtxd0nedgb  30126  wlkvtxedg  30281  pthd  30412  2pthdlem1  30576  clwlkclwwlk  30650  3pthdlem1  30822  frgrregord013  31053  grpoidinvlem3  31165  nmoubi  31431  lnon0  31457  adjsym  32492  nmopub  32567  nmfnleub  32584  cvbr2  32942  chpssati  33022  chrelat2i  33024  chrelat3  33030  mdsymlem8  33069  ralcom4f  33163  reuxfrdf  33186  n0nsnel  33210  uniinn0  33245  ssiun3  33251  disjnf  33262  disjorf  33271  disjunsn  33286  ac6sf2  33314  acunirnmpt2f  33353  nn0min  33508  tosglblem  33631  archiabl  33858  1arithidom  34173  eulerpartlems  35103  eulerpartlemr  35117  eulerpartlemn  35124  ballotlem7  35279  bnj110  35599  bnj92  35603  bnj539  35632  bnj540  35633  bnj580  35654  bnj978  35690  bnj1047  35714  bnj1128  35731  bnj1417  35782  bnj1421  35783  bnj1312  35799  bnj1498  35802  fwfffun  35828  rankse  35864  onvf1od  36076  subfacp1lem3  36155  cvmlift2lem1  36275  cvmlift2lem12  36287  satfv1  36336  fmlaomn0  36363  fmla0disjsuc  36371  fmlasucdisj  36372  mirimanofffr  36670  untuni  36689  dfso3  36700  dffr5  36734  elintfv  36745  elpotr  36758  dfon2lem7  36766  dfon2lem9  36768  dfint3  36931  brlb  36934  dffr7  36935  filnetlem4  37384  axtco  37474  axtco1g  37479  regsfromregtco  37541  mh-infprim3bi  37551  bj-reabeq  38155  bj-axseprep  38260  ctbssinf  38597  fvineqsneq  38603  pibt2  38608  phpreu  38795  ptrecube  38806  poimirlem1  38807  poimirlem25  38831  poimirlem26  38832  poimirlem27  38833  poimirlem30  38836  mblfinlem2  38844  ftc1anc  38887  inixp  38930  ac6gf  38934  heibor1lem  39009  heiborlem1  39011  iscrngo2  39197  ac6s3f  39369  ref5  39517  idinxpssinxp2  39522  n0elqs  39530  ineleq  39552  ralrnmo  39559  ssdmral  39577  refrelcosslem  39750  refrelcoss3  39751  lpssat  40336  lssat  40339  lcvbr2  40345  lcvbr3  40346  lfl1  40393  lub0N  40512  glb0N  40516  atlrelat1  40644  hlrelat2  40726  ispsubsp2  41069  pclclN  41214  cdleme25cv  41681  tendoeq2  42097  cdlemk35  42235  aks4d1p7  43399  sticksstones1  43462  indstrd  43509  supinf  43560  frlmnzcoordex  43918  setindtrs  44298  unielss  44481  ssunib  44483  onsupmaxb  44502  onsupeqnmax  44510  cllem0  44828  ntrneixb  45356  gneispace  45395  expandral  45535  ismnuprim  45539  dfuniv2  45547  undisjrab  45551  zfregs2VD  46083  sswfaxreg  46241  dfac5prim  46244  permac8prim  46268  iindif2f  46448  ralfal  46449  disjinfi  46480  iuneqfzuz  46620  caucvgbf  46772  rexanuz2nf  46775  mccl  46883  limsupub  46987  limsuppnflem  46993  limsupre2lem  47007  lmbr3v  47028  liminfpnfuz  47099  xlimpnfxnegmnf2  47141  ioodvbdlimc1lem2  47215  ioodvbdlimc2lem  47217  dvnprodlem3  47231  fourierdlem103  47492  fourierdlem104  47493  sge0iunmpt  47701  meaiuninc3v  47767  hoidmvle  47883  issmff  48017  n0nsn2el  48368  r19.32  48442  2rexrsb  48446  cbvral2  48447  2reu3  48454  2reu8i  48457  otiunsndisjX  48622  0nelsetpreimafv  48745  dfgric2  49286  gpg5nbgrvtx03starlem1  49439  gpg5nbgrvtx03starlem2  49440  gpg5nbgrvtx03starlem3  49441  gpg5nbgrvtx13starlem1  49442  gpg5nbgrvtx13starlem2  49443  gpg5nbgrvtx13starlem3  49444  gpg5edgnedg  49501  copisnmnd  49539  lindslinindsimp1  49900  lindslinindsimp2  49906  snlindsntor  49914  ldepslinc  49952  iuneq0  50261  iinxp  50273  iscnrm3  50397  ralsbii  51325  ralseubii  51357  aacllem  51367