Theorem ralbii 3084

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

Syntax hints:   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  dfral2  3089  ralinexa  3091  rexanali  3092  r19.26-3  3099  ralbiim  3100  2ralbii  3113  3ralbii  3115  4ralbii  3116  2ralbiim  3117  ralnex2  3118  nrexralim  3122  r19.26-2  3123  r19.23v  3165  r19.32v  3171  2ralor  3212  nelb  3214  cbvral2vw  3220  cbvral3vw  3222  ralrot3  3269  ralcom13  3270  sbralieALT  3325  cbvral2v  3340  cbvral3v  3342  ceqsralv  3483  ralxpxfr2d  3602  reu8  3693  2reuswap  3706  2reu5lem2  3716  2rmoswap  3721  rmoanim  3846  rmoanimALT  3847  dfdif3  4071  dfss5  4229  n0el  4318  ralnralall  4468  2reu4lem  4478  r19.12sn  4679  raldifsnb  4754  eqsn  4787  n0snor2el  4791  uni0b  4891  uni0c  4892  ssint  4921  iuniin  4961  iuneq2  4968  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  5352  otiunsndisj  5476  ssrel2  5742  reliun  5773  xpiindi  5792  rexiunxp  5797  ralxpf  5803  rexxpf  5804  dfse2  6067  idrefALT  6078  asymref2  6082  rninxp  6145  dminxp  6146  cnviin  6252  cnvpo  6253  dfpo2  6262  dfse3  6302  frpoins2fg  6310  dffun9  6529  funcnv3  6570  fncnv  6573  fnres  6627  mptfnf  6635  fnopabg  6637  mptfng  6639  fint  6721  funimass4  6906  fndmdifeq0  6998  funconstss  7010  f1ompt  7065  idref  7101  fconstfv  7168  dff13f  7211  dff14b  7227  weniso  7310  fnssintima  7318  foov  7542  imaeqalov  7607  dfwe2  7729  tfis2f  7808  tfindes  7815  frxp  8078  ralxp3f  8089  frpoins3xpg  8092  frpoins3xp3g  8093  xpord2indlem  8099  xpord3inddlem  8106  soseq  8111  tz7.48lem  8382  tz7.49  8386  oeordi  8525  naddcllem  8614  naddunif  8631  naddasslem2  8633  ixpeq2  8861  ixpin  8873  ixpiin  8874  boxriin  8890  findcard3  9195  fimax2g  9198  fissuni  9269  indexfi  9272  dfsup2  9359  sup0riota  9381  infcllem  9403  wemapsolem  9467  zfinf2  9563  oemapso  9603  ttrclresv  9638  zfregs2  9654  setinds  9670  setinds2f  9671  frins2f  9677  r1elss  9730  rankc1  9794  cp  9815  bnd2  9817  aceq1  10039  aceq2  10041  kmlem7  10079  kmlem12  10084  kmlem13  10085  kmlem15  10087  fin12  10335  ac6num  10401  ac6s2  10408  ac6sf  10411  ac6s4  10412  zorn2lem4  10421  zorn2lem6  10423  zorn2lem7  10424  zorng  10426  ttukeylem6  10436  brdom7disj  10453  brdom6disj  10454  fpwwe2  10566  fpwwe  10569  axgroth5  10747  axgroth4  10755  grothprim  10757  nqereu  10852  dfinfre  12135  infrenegsup  12137  xrsupsslem  13234  xrinfmsslem  13235  xrinfmss2  13238  fzshftral  13543  fsuppmapnn0ub  13930  mptnn0fsuppr  13934  hashgt12el  14357  hashgt12el2  14358  hashbc  14388  s3iunsndisj  14903  cotr2g  14911  rexfiuz  15283  clim0  15441  rpnnen2lem12  16162  gcdcllem1  16438  absproddvds  16556  coprmproddvdslem  16601  vdwmc2  16919  vdwlem13  16933  vdwnn  16938  xpscf  17498  mreacs  17593  acsfn  17594  acsfn1  17596  acsfn2  17598  dfinito2  17939  dftermo2  17940  ispos2  18250  lublecllem  18293  odulub  18340  oduglb  18342  posglbdg  18348  isnmnd  18675  gsumwspan  18783  smndex2dnrinv  18852  isnsg2  19097  oppgid  19297  oppgcntz  19305  efgval2  19665  iscyggen2  19822  iscyg3  19827  oppr1  20298  isnirred  20368  isdomn5  20655  isdomn2OLD  20657  lssne0  20914  iunocv  21648  islindf4  21805  pmatcollpw2lem  22733  isbasis2g  22904  basdif0  22909  tgval2  22912  ntreq0  23033  isclo2  23044  opnnei  23076  neiptopnei  23088  lmres  23256  ist1-3  23305  cmpcov2  23346  cmpsub  23356  is1stc2  23398  1stccn  23419  kgencn  23512  eltx  23524  txkgen  23608  fbun  23796  trfbas  23800  fbunfip  23825  trfil2  23843  isufil2  23864  fixufil  23878  hausflim  23937  txflf  23962  fclsopn  23970  alexsubALTlem3  24005  isclmp  25065  iscau3  25246  iscau4  25247  caucfil  25251  bcth3  25299  ovolgelb  25449  dyadmax  25567  itg2leub  25703  itg2cn  25732  plydivex  26273  vieta1  26288  lgseisenlem2  27355  pnt3  27591  nosepon  27645  nomaxmo  27678  nosupbnd1lem4  27691  conway  27787  eqcuts2  27794  etaslts  27801  lesrec  27807  bday1  27822  cuteq1  27825  madebdaylemlrcut  27907  addsproplem4  27980  addsproplem6  27982  addsprop  27984  addsuniflem  28009  mulsuniflem  28157  oncutlt  28272  oniso  28279  onsfi  28364  bdayn0p1  28377  addhalfcut  28467  tglowdim2ln  28735  axcontlem12  29060  elntg2  29070  numedglnl  29229  vtxd0nedgb  29574  wlkvtxedg  29729  pthd  29854  2pthdlem1  30015  clwlkclwwlk  30089  3pthdlem1  30251  frgrregord013  30482  grpoidinvlem3  30594  nmoubi  30860  lnon0  30886  adjsym  31921  nmopub  31996  nmfnleub  32013  cvbr2  32371  chpssati  32451  chrelat2i  32453  chrelat3  32459  mdsymlem8  32498  ralcom4f  32553  reuxfrdf  32577  n0nsnel  32602  uniinn0  32637  ssiun3  32645  disjnf  32657  disjorf  32666  disjunsn  32681  ac6sf2  32712  nn0min  32912  tosglblem  33067  archiabl  33292  1arithidom  33630  eulerpartlems  34538  eulerpartlemr  34552  eulerpartlemn  34559  ballotlem7  34714  bnj110  35034  bnj92  35038  bnj539  35067  bnj540  35068  bnj580  35089  bnj978  35125  bnj1047  35149  bnj1128  35166  bnj1417  35217  bnj1421  35218  bnj1312  35234  bnj1498  35237  onvf1od  35323  lfuhgr3  35336  subfacp1lem3  35398  cvmlift2lem1  35518  cvmlift2lem12  35530  satfv1  35579  fmlaomn0  35606  fmla0disjsuc  35614  fmlasucdisj  35615  untuni  35925  dfso3  35936  elintfv  35981  elpotr  35995  dfon2lem7  36003  dfon2lem9  36005  dfint3  36168  brlb  36171  filnetlem4  36597  regsfromregtr  36690  bj-reabeq  37275  bj-axseprep  37322  ctbssinf  37661  fvineqsneq  37667  pibt2  37672  phpreu  37855  ptrecube  37871  poimirlem1  37872  poimirlem25  37896  poimirlem26  37897  poimirlem27  37898  poimirlem30  37901  mblfinlem2  37909  ftc1anc  37952  inixp  37979  ac6gf  37983  heibor1lem  38060  heiborlem1  38062  iscrngo2  38248  ac6s3f  38422  ref5  38570  idinxpssinxp2  38575  n0elqs  38583  ineleq  38605  ralrnmo  38612  ssdmral  38630  refrelcosslem  38803  refrelcoss3  38804  lpssat  39389  lssat  39392  lcvbr2  39398  lcvbr3  39399  lfl1  39446  lub0N  39565  glb0N  39569  atlrelat1  39697  hlrelat2  39779  ispsubsp2  40122  pclclN  40267  cdleme25cv  40734  tendoeq2  41150  cdlemk35  41288  aks4d1p7  42453  sticksstones1  42516  indstrd  42563  supinf  42612  infdesc  43001  setindtrs  43382  unielss  43575  ssunib  43577  onsupmaxb  43596  onsupeqnmax  43604  cllem0  43922  ntrneixb  44451  gneispace  44490  expandral  44646  ismnuprim  44650  dfuniv2  44658  undisjrab  44662  zfregs2VD  45196  sswfaxreg  45343  dfac5prim  45346  permac8prim  45370  iindif2f  45519  ralfal  45520  disjinfi  45551  iuneqfzuz  45694  caucvgbf  45847  rexanuz2nf  45850  mccl  45958  limsupub  46062  limsuppnflem  46068  limsupre2lem  46082  lmbr3v  46103  liminfpnfuz  46174  xlimpnfxnegmnf2  46216  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnprodlem3  46306  fourierdlem103  46567  fourierdlem104  46568  sge0iunmpt  46776  meaiuninc3v  46842  hoidmvle  46958  issmff  47092  n0nsn2el  47385  r19.32  47458  2rexrsb  47462  cbvral2  47463  2reu3  47470  2reu8i  47473  otiunsndisjX  47639  0nelsetpreimafv  47750  dfgric2  48275  gpg5nbgrvtx03starlem1  48428  gpg5nbgrvtx03starlem2  48429  gpg5nbgrvtx03starlem3  48430  gpg5nbgrvtx13starlem1  48431  gpg5nbgrvtx13starlem2  48432  gpg5nbgrvtx13starlem3  48433  gpg5edgnedg  48490  copisnmnd  48529  lindslinindsimp1  48817  lindslinindsimp2  48823  snlindsntor  48831  ldepslinc  48869  iuneq0  49178  iinxp  49190  iscnrm3  49311  setrec1lem3  50048  aacllem  50160