Theorem ralbii 3090

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

Syntax hints:   ↔ wb 206   ∈ wcel 2105  ∀wral 3058

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

This theorem depends on definitions:  df-bi 207  df-ral 3059

This theorem is referenced by:  dfral2  3096  ralinexa  3098  rexanali  3099  rexbiOLD  3102  r19.26-3  3109  ralbiim  3110  2ralbii  3125  3ralbii  3127  4ralbii  3128  2ralbiim  3129  ralnex2  3130  nrexralim  3134  r19.26-2  3135  r19.23v  3180  r19.32v  3189  2ralor  3228  nelb  3231  nelbOLD  3232  cbvral2vw  3238  cbvral3vw  3240  ralrot3  3290  ralcom13  3291  ralcom13OLD  3292  sbralieALT  3356  cbvral2v  3365  cbvral3v  3367  moelOLD  3402  ceqsralv  3519  ralxpxfr2d  3645  reu8  3741  2reuswap  3754  2reu5lem2  3764  2rmoswap  3769  rmoanim  3902  rmoanimALT  3903  dfdif3  4126  dfss5  4280  n0el  4369  ralnralall  4520  2reu4lem  4527  r19.12sn  4724  raldifsnb  4800  eqsn  4833  n0snor2el  4837  uni0b  4937  uni0c  4938  ssint  4968  iuniin  5008  iuneq2  5015  iunssf  5048  iunss  5049  ssiinf  5058  iinab  5072  iinun2  5077  iindif1  5079  iindif2  5081  iinin2  5082  iinuni  5102  sspwuni  5104  iinpw  5110  disjor  5129  disjxun  5145  dftr3  5270  reusv3  5410  otiunsndisj  5529  ssrel2  5797  reliun  5828  xpiindi  5848  rexiunxp  5853  ralxpf  5859  rexxpf  5860  dfse2  6120  idrefALT  6133  asymref2  6139  rninxp  6200  dminxp  6201  cnviin  6307  cnvpo  6308  dfpo2  6317  dfse3  6358  frpoins2fg  6366  wfis2fgOLD  6379  dffun9  6596  funcnv3  6637  fncnv  6640  fnres  6695  mptfnf  6703  fnopabg  6705  mptfng  6707  fint  6787  funimass4  6972  fndmdifeq0  7063  funconstss  7075  f1ompt  7130  idref  7165  fconstfv  7231  dff13f  7275  dff14b  7290  weniso  7373  fnssintima  7381  foov  7606  imaeqalov  7671  dfwe2  7792  tfis2f  7876  tfindes  7883  frxp  8149  ralxp3f  8160  frpoins3xpg  8163  frpoins3xp3g  8164  xpord2indlem  8170  xpord3inddlem  8177  soseq  8182  dfwrecsOLD  8336  tz7.48lem  8479  tz7.49  8483  oeordi  8623  naddcllem  8712  naddunif  8729  naddasslem2  8731  ixpeq2  8949  ixpin  8961  ixpiin  8962  boxriin  8978  findcard3  9315  findcard3OLD  9316  fimax2g  9319  fissuni  9394  indexfi  9397  dfsup2  9481  sup0riota  9502  infcllem  9524  wemapsolem  9587  zfinf2  9679  oemapso  9719  ttrclresv  9754  zfregs2  9770  frins2f  9790  r1elss  9843  rankc1  9907  cp  9928  bnd2  9930  aceq1  10154  aceq2  10156  kmlem7  10194  kmlem12  10199  kmlem13  10200  kmlem15  10202  fin12  10450  ac6num  10516  ac6s2  10523  ac6sf  10526  ac6s4  10527  zorn2lem4  10536  zorn2lem6  10538  zorn2lem7  10539  zorng  10541  ttukeylem6  10551  brdom7disj  10568  brdom6disj  10569  fpwwe2  10680  fpwwe  10683  axgroth5  10861  axgroth4  10869  grothprim  10871  nqereu  10966  dfinfre  12246  infrenegsup  12248  xrsupsslem  13345  xrinfmsslem  13346  xrinfmss2  13349  fzshftral  13651  fsuppmapnn0ub  14032  mptnn0fsuppr  14036  hashgt12el  14457  hashgt12el2  14458  hashbc  14488  s3iunsndisj  15003  cotr2g  15011  rexfiuz  15382  clim0  15538  rpnnen2lem12  16257  gcdcllem1  16532  absproddvds  16650  coprmproddvdslem  16695  vdwmc2  17012  vdwlem13  17026  vdwnn  17031  xpscf  17611  mreacs  17702  acsfn  17703  acsfn1  17705  acsfn2  17707  dfinito2  18056  dftermo2  18057  ispos2  18372  lublecllem  18417  odulub  18464  oduglb  18466  posglbdg  18472  isnmnd  18763  gsumwspan  18871  smndex2dnrinv  18940  isnsg2  19186  oppgid  19389  oppgcntz  19397  efgval2  19756  iscyggen2  19913  iscyg3  19918  oppr1  20366  isnirred  20436  isdomn5  20726  isdomn2OLD  20728  lssne0  20966  iunocv  21716  islindf4  21875  pmatcollpw2lem  22798  isbasis2g  22970  basdif0  22975  tgval2  22978  ntreq0  23100  isclo2  23111  opnnei  23143  neiptopnei  23155  lmres  23323  ist1-3  23372  cmpcov2  23413  cmpsub  23423  is1stc2  23465  1stccn  23486  kgencn  23579  eltx  23591  txkgen  23675  fbun  23863  trfbas  23867  fbunfip  23892  trfil2  23910  isufil2  23931  fixufil  23945  hausflim  24004  txflf  24029  fclsopn  24037  alexsubALTlem3  24072  isclmp  25143  iscau3  25325  iscau4  25326  caucfil  25330  bcth3  25378  ovolgelb  25528  dyadmax  25646  itg2leub  25783  itg2cn  25812  plydivex  26353  vieta1  26368  lgseisenlem2  27434  pnt3  27670  nosepon  27724  nomaxmo  27757  nosupbnd1lem4  27770  conway  27858  eqscut2  27865  etasslt  27872  slerec  27878  bday1s  27890  cuteq1  27892  madebdaylemlrcut  27951  addsproplem4  28019  addsproplem6  28021  addsprop  28023  addsuniflem  28048  mulsuniflem  28189  halfcut  28430  addhalfcut  28433  tglowdim2ln  28673  axcontlem12  29004  elntg2  29014  numedglnl  29175  vtxd0nedgb  29520  wlkvtxedg  29676  pthd  29801  2pthdlem1  29959  clwlkclwwlk  30030  3pthdlem1  30192  frgrregord013  30423  grpoidinvlem3  30534  nmoubi  30800  lnon0  30826  adjsym  31861  nmopub  31936  nmfnleub  31953  cvbr2  32311  chpssati  32391  chrelat2i  32393  chrelat3  32399  mdsymlem8  32438  ralcom4f  32495  reuxfrdf  32518  n0nsnel  32542  uniinn0  32570  ssiun3  32578  disjnf  32589  disjorf  32598  disjunsn  32613  ac6sf2  32641  nn0min  32826  tosglblem  32948  archiabl  33187  1arithidom  33544  eulerpartlems  34341  eulerpartlemr  34355  eulerpartlemn  34362  ballotlem7  34516  bnj110  34850  bnj92  34854  bnj539  34883  bnj540  34884  bnj580  34905  bnj978  34941  bnj1047  34965  bnj1128  34982  bnj1417  35033  bnj1421  35034  bnj1312  35050  bnj1498  35053  lfuhgr3  35103  subfacp1lem3  35166  cvmlift2lem1  35286  cvmlift2lem12  35298  satfv1  35347  fmlaomn0  35374  fmla0disjsuc  35382  fmlasucdisj  35383  untuni  35688  dfso3  35699  elintfv  35745  setinds  35759  setinds2f  35760  elpotr  35762  dfon2lem7  35770  dfon2lem9  35772  dfint3  35933  brlb  35936  filnetlem4  36363  bj-reabeq  37009  ctbssinf  37388  fvineqsneq  37394  pibt2  37399  phpreu  37590  ptrecube  37606  poimirlem1  37607  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem30  37636  mblfinlem2  37644  ftc1anc  37687  inixp  37714  ac6gf  37718  heibor1lem  37795  heiborlem1  37797  iscrngo2  37983  ac6s3f  38157  ref5  38294  idinxpssinxp2  38299  n0elqs  38307  ineleq  38335  refrelcosslem  38443  refrelcoss3  38444  lpssat  38994  lssat  38997  lcvbr2  39003  lcvbr3  39004  lfl1  39051  lub0N  39170  glb0N  39174  atlrelat1  39302  hlrelat2  39385  ispsubsp2  39728  pclclN  39873  cdleme25cv  40340  tendoeq2  40756  cdlemk35  40894  aks4d1p7  42064  sticksstones1  42127  indstrd  42174  supinf  42261  infdesc  42629  setindtrs  43013  unielss  43206  ssunib  43208  onsupmaxb  43227  onsupeqnmax  43235  cllem0  43555  ntrneixb  44084  gneispace  44123  expandral  44285  ismnuprim  44289  dfuniv2  44297  undisjrab  44301  zfregs2VD  44838  iindif2f  45102  ralfal  45103  disjinfi  45134  iuneqfzuz  45284  caucvgbf  45439  rexanuz2nf  45442  mccl  45553  limsupub  45659  limsuppnflem  45665  limsupre2lem  45679  lmbr3v  45700  liminfpnfuz  45771  xlimpnfxnegmnf2  45813  ioodvbdlimc1lem2  45887  ioodvbdlimc2lem  45889  dvnprodlem3  45903  fourierdlem103  46164  fourierdlem104  46165  sge0iunmpt  46373  meaiuninc3v  46439  hoidmvle  46555  issmff  46689  n0nsn2el  46974  r19.32  47047  2rexrsb  47051  cbvral2  47052  2reu3  47059  2reu8i  47062  otiunsndisjX  47228  0nelsetpreimafv  47314  dfgric2  47821  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  copisnmnd  48012  lindslinindsimp1  48302  lindslinindsimp2  48308  snlindsntor  48316  ldepslinc  48354  iscnrm3  48748  setrec1lem3  48919  aacllem  49031