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  3317  cbvral2v  3331  cbvral3v  3333  ceqsralv  3471  ralxpxfr2d  3589  reu8  3680  2reuswap  3693  2reu5lem2  3703  2rmoswap  3708  rmoanim  3833  rmoanimALT  3834  dfdif3  4058  dfss5  4216  n0el  4305  ralnralall  4454  2reu4lem  4464  r19.12sn  4665  raldifsnb  4740  eqsn  4773  n0snor2el  4777  uni0b  4877  uni0c  4878  ssint  4907  iuniin  4947  iuneq2  4954  iunssf  4986  iunssfOLD  4987  iunss  4988  iunssOLD  4989  ssiinf  4998  iinab  5011  iinun2  5016  iindif1  5018  iindif2  5020  iinin2  5021  iinuni  5041  sspwuni  5043  iinpw  5049  disjor  5068  disjxun  5084  dftr3  5198  reusv3  5343  otiunsndisj  5469  ssrel2  5735  reliun  5766  xpiindi  5785  rexiunxp  5790  ralxpf  5796  rexxpf  5797  dfse2  6060  idrefALT  6071  asymref2  6075  rninxp  6138  dminxp  6139  cnviin  6245  cnvpo  6246  dfpo2  6255  dfse3  6295  frpoins2fg  6303  dffun9  6522  funcnv3  6563  fncnv  6566  fnres  6620  mptfnf  6628  fnopabg  6630  mptfng  6632  fint  6714  funimass4  6899  fndmdifeq0  6991  funconstss  7003  f1ompt  7058  idref  7094  fconstfv  7161  dff13f  7204  dff14b  7220  weniso  7303  fnssintima  7311  foov  7535  imaeqalov  7600  dfwe2  7722  tfis2f  7801  tfindes  7808  frxp  8070  ralxp3f  8081  frpoins3xpg  8084  frpoins3xp3g  8085  xpord2indlem  8091  xpord3inddlem  8098  soseq  8103  tz7.48lem  8374  tz7.49  8378  oeordi  8517  naddcllem  8606  naddunif  8623  naddasslem2  8625  ixpeq2  8853  ixpin  8865  ixpiin  8866  boxriin  8882  findcard3  9187  fimax2g  9190  fissuni  9261  indexfi  9264  dfsup2  9351  sup0riota  9373  infcllem  9395  wemapsolem  9459  zfinf2  9557  oemapso  9597  ttrclresv  9632  zfregs2  9648  setinds  9664  setinds2f  9665  frins2f  9671  r1elss  9724  rankc1  9788  cp  9809  bnd2  9811  aceq1  10033  aceq2  10035  kmlem7  10073  kmlem12  10078  kmlem13  10079  kmlem15  10081  fin12  10329  ac6num  10395  ac6s2  10402  ac6sf  10405  ac6s4  10406  zorn2lem4  10415  zorn2lem6  10417  zorn2lem7  10418  zorng  10420  ttukeylem6  10430  brdom7disj  10447  brdom6disj  10448  fpwwe2  10560  fpwwe  10563  axgroth5  10741  axgroth4  10749  grothprim  10751  nqereu  10846  dfinfre  12131  infrenegsup  12133  xrsupsslem  13253  xrinfmsslem  13254  xrinfmss2  13257  fzshftral  13563  fsuppmapnn0ub  13951  mptnn0fsuppr  13955  hashgt12el  14378  hashgt12el2  14379  hashbc  14409  s3iunsndisj  14924  cotr2g  14932  rexfiuz  15304  clim0  15462  rpnnen2lem12  16186  gcdcllem1  16462  absproddvds  16580  coprmproddvdslem  16625  vdwmc2  16944  vdwlem13  16958  vdwnn  16963  xpscf  17523  mreacs  17618  acsfn  17619  acsfn1  17621  acsfn2  17623  dfinito2  17964  dftermo2  17965  ispos2  18275  lublecllem  18318  odulub  18365  oduglb  18367  posglbdg  18373  isnmnd  18700  gsumwspan  18808  smndex2dnrinv  18880  isnsg2  19125  oppgid  19325  oppgcntz  19333  efgval2  19693  iscyggen2  19850  iscyg3  19855  oppr1  20324  isnirred  20394  isdomn5  20681  isdomn2OLD  20683  lssne0  20940  iunocv  21674  islindf4  21831  pmatcollpw2lem  22755  isbasis2g  22926  basdif0  22931  tgval2  22934  ntreq0  23055  isclo2  23066  opnnei  23098  neiptopnei  23110  lmres  23278  ist1-3  23327  cmpcov2  23368  cmpsub  23378  is1stc2  23420  1stccn  23441  kgencn  23534  eltx  23546  txkgen  23630  fbun  23818  trfbas  23822  fbunfip  23847  trfil2  23865  isufil2  23886  fixufil  23900  hausflim  23959  txflf  23984  fclsopn  23992  alexsubALTlem3  24027  isclmp  25077  iscau3  25258  iscau4  25259  caucfil  25263  bcth3  25311  ovolgelb  25460  dyadmax  25578  itg2leub  25714  itg2cn  25743  plydivex  26277  vieta1  26292  lgseisenlem2  27356  pnt3  27592  nosepon  27646  nomaxmo  27679  nosupbnd1lem4  27692  conway  27788  eqcuts2  27795  etaslts  27802  lesrec  27808  bday1  27823  cuteq1  27826  madebdaylemlrcut  27908  addsproplem4  27981  addsproplem6  27983  addsprop  27985  addsuniflem  28010  mulsuniflem  28158  oncutlt  28273  oniso  28280  onsfi  28365  bdayn0p1  28378  addhalfcut  28468  tglowdim2ln  28736  axcontlem12  29061  elntg2  29071  numedglnl  29230  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  32638  ssiun3  32646  disjnf  32658  disjorf  32667  disjunsn  32682  ac6sf2  32713  nn0min  32912  tosglblem  33052  archiabl  33277  1arithidom  33615  eulerpartlems  34523  eulerpartlemr  34537  eulerpartlemn  34544  ballotlem7  34699  bnj110  35019  bnj92  35023  bnj539  35052  bnj540  35053  bnj580  35074  bnj978  35110  bnj1047  35134  bnj1128  35151  bnj1417  35202  bnj1421  35203  bnj1312  35219  bnj1498  35222  onvf1od  35308  lfuhgr3  35321  subfacp1lem3  35383  cvmlift2lem1  35503  cvmlift2lem12  35515  satfv1  35564  fmlaomn0  35591  fmla0disjsuc  35599  fmlasucdisj  35600  untuni  35910  dfso3  35921  elintfv  35966  elpotr  35980  dfon2lem7  35988  dfon2lem9  35990  dfint3  36153  brlb  36156  filnetlem4  36582  axtco  36672  axtco1g  36677  regsfromregtco  36739  mh-infprim3bi  36749  bj-reabeq  37353  bj-axseprep  37400  ctbssinf  37739  fvineqsneq  37745  pibt2  37750  phpreu  37942  ptrecube  37958  poimirlem1  37959  poimirlem25  37983  poimirlem26  37984  poimirlem27  37985  poimirlem30  37988  mblfinlem2  37996  ftc1anc  38039  inixp  38066  ac6gf  38070  heibor1lem  38147  heiborlem1  38149  iscrngo2  38335  ac6s3f  38509  ref5  38657  idinxpssinxp2  38662  n0elqs  38670  ineleq  38692  ralrnmo  38699  ssdmral  38717  refrelcosslem  38890  refrelcoss3  38891  lpssat  39476  lssat  39479  lcvbr2  39485  lcvbr3  39486  lfl1  39533  lub0N  39652  glb0N  39656  atlrelat1  39784  hlrelat2  39866  ispsubsp2  40209  pclclN  40354  cdleme25cv  40821  tendoeq2  41237  cdlemk35  41375  aks4d1p7  42539  sticksstones1  42602  indstrd  42649  supinf  42698  infdesc  43093  setindtrs  43474  unielss  43667  ssunib  43669  onsupmaxb  43688  onsupeqnmax  43696  cllem0  44014  ntrneixb  44543  gneispace  44582  expandral  44738  ismnuprim  44742  dfuniv2  44750  undisjrab  44754  zfregs2VD  45288  sswfaxreg  45435  dfac5prim  45438  permac8prim  45462  iindif2f  45611  ralfal  45612  disjinfi  45643  iuneqfzuz  45786  caucvgbf  45938  rexanuz2nf  45941  mccl  46049  limsupub  46153  limsuppnflem  46159  limsupre2lem  46173  lmbr3v  46194  liminfpnfuz  46265  xlimpnfxnegmnf2  46307  ioodvbdlimc1lem2  46381  ioodvbdlimc2lem  46383  dvnprodlem3  46397  fourierdlem103  46658  fourierdlem104  46659  sge0iunmpt  46867  meaiuninc3v  46933  hoidmvle  47049  issmff  47183  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