Theorem ralbii 3085

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

Syntax hints:   ↔ wb 207   ∈ wcel 2119  ∀wral 3053

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

This theorem depends on definitions:  df-bi 208  df-ral 3054

This theorem is referenced by:  dfral2  3090  ralinexa  3092  rexanali  3093  r19.26-3  3100  ralbiim  3101  2ralbii  3114  3ralbii  3116  4ralbii  3117  2ralbiim  3118  ralnex2  3119  nrexralim  3123  r19.26-2  3124  r19.23v  3166  r19.32v  3172  2ralor  3213  nelb  3215  cbvral2vw  3221  cbvral3vw  3223  ralrot3  3270  ralcom13  3271  sbralieALT  3318  cbvral2v  3332  cbvral3v  3334  ceqsralv  3471  ralxpxfr2d  3584  reu8  3674  2reuswap  3687  2reu5lem2  3697  2rmoswap  3702  rmoanim  3826  rmoanimALT  3827  dfdif3  4048  dfss5  4203  n0el  4292  ralnralall  4441  2reu4lem  4451  r19.12sn  4652  raldifsnb  4729  eqsn  4760  n0snor2el  4764  uni0b  4864  uni0c  4865  ssint  4894  iuniin  4934  iuneq2  4941  iunssf  4972  iunssfOLD  4973  iunss  4974  iunssOLD  4975  ssiinf  4984  iinab  4997  iinun2  5002  iindif1  5004  iindif2  5006  iinin2  5007  iinuni  5027  sspwuni  5029  iinpw  5035  disjor  5054  disjxun  5070  dftr3  5184  reusv3  5334  otiunsndisj  5461  ssrel2  5728  reliun  5759  xpiindi  5777  rexiunxp  5782  ralxpf  5788  rexxpf  5789  dfse2  6052  idrefALT  6063  asymref2  6067  rninxp  6130  dminxp  6131  cnviin  6237  cnvpo  6238  dfpo2  6247  dfse3  6287  frpoins2fg  6295  dffun9  6514  funcnv3  6555  fncnv  6558  fnres  6612  mptfnf  6620  fnopabg  6622  mptfng  6624  fint  6706  funimass4  6891  fndmdifeq0  6985  funconstss  6997  f1ompt  7052  idref  7088  fconstfv  7156  dff13f  7199  dff14b  7215  weniso  7298  fnssintima  7306  foov  7530  imaeqalov  7595  dfwe2  7717  tfis2f  7796  tfindes  7803  frxp  8066  ralxp3f  8077  frpoins3xpg  8080  frpoins3xp3g  8081  xpord2indlem  8087  xpord3inddlem  8094  soseq  8099  tz7.48lem  8370  tz7.49  8374  oeordi  8513  naddcllem  8602  naddunif  8619  naddasslem2  8621  ixpeq2  8849  ixpin  8861  ixpiin  8862  boxriin  8878  findcard3  9183  fimax2g  9186  fissuni  9257  indexfi  9260  dfsup2  9347  sup0riota  9369  infcllem  9391  wemapsolem  9455  zfinf2  9554  oemapso  9594  ttrclresv  9629  zfregs2  9645  setinds  9661  setinds2f  9662  frins2f  9668  r1elss  9721  rankc1  9785  cp  9806  bnd2  9808  aceq1  10030  aceq2  10032  kmlem7  10070  kmlem12  10075  kmlem13  10076  kmlem15  10078  fin12  10326  ac6num  10392  ac6s2  10399  ac6sf  10402  ac6s4  10403  zorn2lem4  10412  zorn2lem6  10414  zorn2lem7  10415  zorng  10417  ttukeylem6  10427  brdom7disj  10444  brdom6disj  10445  fpwwe2  10557  fpwwe  10560  axgroth5  10738  axgroth4  10746  grothprim  10748  nqereu  10843  dfinfre  12128  infrenegsup  12130  xrsupsslem  13250  xrinfmsslem  13251  xrinfmss2  13254  fzshftral  13560  fsuppmapnn0ub  13948  mptnn0fsuppr  13952  hashgt12el  14375  hashgt12el2  14376  hashbc  14406  s3iunsndisj  14921  cotr2g  14929  rexfiuz  15301  clim0  15459  rpnnen2lem12  16183  gcdcllem1  16459  absproddvds  16577  coprmproddvdslem  16622  vdwmc2  16941  vdwlem13  16955  vdwnn  16960  xpscf  17520  mreacs  17615  acsfn  17616  acsfn1  17618  acsfn2  17620  dfinito2  17961  dftermo2  17962  ispos2  18272  lublecllem  18315  odulub  18362  oduglb  18364  posglbdg  18370  isnmnd  18697  gsumwspan  18805  smndex2dnrinv  18877  isnsg2  19122  oppgid  19322  oppgcntz  19330  efgval2  19690  iscyggen2  19847  iscyg3  19852  oppr1  20321  isnirred  20391  isdomn5  20682  isdomn2OLD  20684  lssne0  20941  iunocv  21656  islindf4  21813  pmatcollpw2lem  22760  isbasis2g  22931  basdif0  22936  tgval2  22939  ntreq0  23060  isclo2  23071  opnnei  23103  neiptopnei  23115  lmres  23283  ist1-3  23332  cmpcov2  23373  cmpsub  23383  is1stc2  23425  1stccn  23446  kgencn  23539  eltx  23551  txkgen  23635  fbun  23823  trfbas  23827  fbunfip  23852  trfil2  23870  isufil2  23891  fixufil  23905  hausflim  23964  txflf  23989  fclsopn  23997  alexsubALTlem3  24032  isclmp  25082  iscau3  25263  iscau4  25264  caucfil  25268  bcth3  25316  ovolgelb  25465  dyadmax  25583  itg2leub  25719  itg2cn  25748  plydivex  26281  vieta1  26296  lgseisenlem2  27357  pnt3  27593  nosepon  27647  nomaxmo  27680  nosupbnd1lem4  27693  conway  27789  eqcuts2  27796  etaslts  27803  lesrec  27809  bday1  27824  cuteq1  27827  madebdaylemlrcut  27909  addsproplem4  27982  addsproplem6  27984  addsprop  27986  addsuniflem  28011  mulsuniflem  28159  oncutlt  28274  oniso  28281  onsfi  28366  bdayn0p1  28379  addhalfcut  28469  tglowdim2ln  28737  axcontlem12  29062  elntg2  29072  numedglnl  29231  vtxd0nedgb  29575  wlkvtxedg  29730  pthd  29855  2pthdlem1  30016  clwlkclwwlk  30090  3pthdlem1  30252  frgrregord013  30483  grpoidinvlem3  30595  nmoubi  30861  lnon0  30887  adjsym  31922  nmopub  31997  nmfnleub  32014  cvbr2  32372  chpssati  32452  chrelat2i  32454  chrelat3  32460  mdsymlem8  32499  ralcom4f  32554  reuxfrdf  32578  n0nsnel  32603  uniinn0  32639  ssiun3  32647  disjnf  32659  disjorf  32668  disjunsn  32683  ac6sf2  32714  nn0min  32913  tosglblem  33053  archiabl  33279  1arithidom  33620  eulerpartlems  34544  eulerpartlemr  34558  eulerpartlemn  34565  ballotlem7  34720  bnj110  35040  bnj92  35044  bnj539  35073  bnj540  35074  bnj580  35095  bnj978  35131  bnj1047  35155  bnj1128  35172  bnj1417  35223  bnj1421  35224  bnj1312  35240  bnj1498  35243  onvf1od  35335  lfuhgr3  35348  subfacp1lem3  35410  cvmlift2lem1  35530  cvmlift2lem12  35542  satfv1  35591  fmlaomn0  35618  fmla0disjsuc  35626  fmlasucdisj  35627  untuni  35937  dfso3  35948  elintfv  35993  elpotr  36007  dfon2lem7  36015  dfon2lem9  36017  dfint3  36180  brlb  36183  filnetlem4  36609  axtco  36699  axtco1g  36704  regsfromregtco  36766  mh-infprim3bi  36776  bj-reabeq  37380  bj-axseprep  37427  ctbssinf  37768  fvineqsneq  37774  pibt2  37779  phpreu  37971  ptrecube  37987  poimirlem1  37988  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem30  38017  mblfinlem2  38025  ftc1anc  38068  inixp  38095  ac6gf  38099  heibor1lem  38176  heiborlem1  38178  iscrngo2  38364  ac6s3f  38538  ref5  38686  idinxpssinxp2  38691  n0elqs  38699  ineleq  38721  ralrnmo  38728  ssdmral  38746  refrelcosslem  38919  refrelcoss3  38920  lpssat  39505  lssat  39508  lcvbr2  39514  lcvbr3  39515  lfl1  39562  lub0N  39681  glb0N  39685  atlrelat1  39813  hlrelat2  39895  ispsubsp2  40238  pclclN  40383  cdleme25cv  40850  tendoeq2  41266  cdlemk35  41404  aks4d1p7  42568  sticksstones1  42631  indstrd  42678  supinf  42726  infdesc  43093  setindtrs  43470  unielss  43663  ssunib  43665  onsupmaxb  43684  onsupeqnmax  43692  cllem0  44010  ntrneixb  44539  gneispace  44578  expandral  44734  ismnuprim  44738  dfuniv2  44746  undisjrab  44750  zfregs2VD  45284  sswfaxreg  45431  dfac5prim  45434  permac8prim  45458  iindif2f  45607  ralfal  45608  disjinfi  45639  iuneqfzuz  45780  caucvgbf  45932  rexanuz2nf  45935  mccl  46043  limsupub  46147  limsuppnflem  46153  limsupre2lem  46167  lmbr3v  46188  liminfpnfuz  46259  xlimpnfxnegmnf2  46301  ioodvbdlimc1lem2  46375  ioodvbdlimc2lem  46377  dvnprodlem3  46391  fourierdlem103  46652  fourierdlem104  46653  sge0iunmpt  46861  meaiuninc3v  46927  hoidmvle  47043  issmff  47177  n0nsn2el  47488  r19.32  47561  2rexrsb  47565  cbvral2  47566  2reu3  47573  2reu8i  47576  otiunsndisjX  47742  0nelsetpreimafv  47865  dfgric2  48406  gpg5nbgrvtx03starlem1  48559  gpg5nbgrvtx03starlem2  48560  gpg5nbgrvtx03starlem3  48561  gpg5nbgrvtx13starlem1  48562  gpg5nbgrvtx13starlem2  48563  gpg5nbgrvtx13starlem3  48564  gpg5edgnedg  48621  copisnmnd  48660  lindslinindsimp1  48948  lindslinindsimp2  48954  snlindsntor  48962  ldepslinc  49000  iuneq0  49309  iinxp  49321  iscnrm3  49442  setrec1lem3  50179  aacllem  50291