Theorem ralbii 3080

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∀wral 3049

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

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

This theorem is referenced by:  dfral2  3085  ralinexa  3087  rexanali  3088  r19.26-3  3095  ralbiim  3096  2ralbii  3109  3ralbii  3111  4ralbii  3112  2ralbiim  3113  ralnex2  3114  nrexralim  3118  r19.26-2  3119  r19.23v  3161  r19.32v  3167  2ralor  3208  nelb  3210  cbvral2vw  3216  cbvral3vw  3218  ralrot3  3265  ralcom13  3266  sbralieALT  3321  cbvral2v  3336  cbvral3v  3338  ceqsralv  3479  ralxpxfr2d  3598  reu8  3689  2reuswap  3702  2reu5lem2  3712  2rmoswap  3717  rmoanim  3842  rmoanimALT  3843  dfdif3  4067  dfss5  4225  n0el  4314  ralnralall  4464  2reu4lem  4474  r19.12sn  4675  raldifsnb  4750  eqsn  4783  n0snor2el  4787  uni0b  4887  uni0c  4888  ssint  4917  iuniin  4957  iuneq2  4964  iunssf  4996  iunssfOLD  4997  iunss  4998  iunssOLD  4999  ssiinf  5008  iinab  5021  iinun2  5026  iindif1  5028  iindif2  5030  iinin2  5031  iinuni  5051  sspwuni  5053  iinpw  5059  disjor  5078  disjxun  5094  dftr3  5208  reusv3  5348  otiunsndisj  5466  ssrel2  5732  reliun  5763  xpiindi  5782  rexiunxp  5787  ralxpf  5793  rexxpf  5794  dfse2  6057  idrefALT  6068  asymref2  6072  rninxp  6135  dminxp  6136  cnviin  6242  cnvpo  6243  dfpo2  6252  dfse3  6292  frpoins2fg  6300  dffun9  6519  funcnv3  6560  fncnv  6563  fnres  6617  mptfnf  6625  fnopabg  6627  mptfng  6629  fint  6711  funimass4  6896  fndmdifeq0  6987  funconstss  6999  f1ompt  7054  idref  7089  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  8847  ixpin  8859  ixpiin  8860  boxriin  8876  findcard3  9181  fimax2g  9184  fissuni  9255  indexfi  9258  dfsup2  9345  sup0riota  9367  infcllem  9389  wemapsolem  9453  zfinf2  9549  oemapso  9589  ttrclresv  9624  zfregs2  9640  setinds  9656  setinds2f  9657  frins2f  9663  r1elss  9716  rankc1  9780  cp  9801  bnd2  9803  aceq1  10025  aceq2  10027  kmlem7  10065  kmlem12  10070  kmlem13  10071  kmlem15  10073  fin12  10321  ac6num  10387  ac6s2  10394  ac6sf  10397  ac6s4  10398  zorn2lem4  10407  zorn2lem6  10409  zorn2lem7  10410  zorng  10412  ttukeylem6  10422  brdom7disj  10439  brdom6disj  10440  fpwwe2  10552  fpwwe  10555  axgroth5  10733  axgroth4  10741  grothprim  10743  nqereu  10838  dfinfre  12121  infrenegsup  12123  xrsupsslem  13220  xrinfmsslem  13221  xrinfmss2  13224  fzshftral  13529  fsuppmapnn0ub  13916  mptnn0fsuppr  13920  hashgt12el  14343  hashgt12el2  14344  hashbc  14374  s3iunsndisj  14889  cotr2g  14897  rexfiuz  15269  clim0  15427  rpnnen2lem12  16148  gcdcllem1  16424  absproddvds  16542  coprmproddvdslem  16587  vdwmc2  16905  vdwlem13  16919  vdwnn  16924  xpscf  17484  mreacs  17579  acsfn  17580  acsfn1  17582  acsfn2  17584  dfinito2  17925  dftermo2  17926  ispos2  18236  lublecllem  18279  odulub  18326  oduglb  18328  posglbdg  18334  isnmnd  18661  gsumwspan  18769  smndex2dnrinv  18838  isnsg2  19083  oppgid  19283  oppgcntz  19291  efgval2  19651  iscyggen2  19808  iscyg3  19813  oppr1  20284  isnirred  20354  isdomn5  20641  isdomn2OLD  20643  lssne0  20900  iunocv  21634  islindf4  21791  pmatcollpw2lem  22719  isbasis2g  22890  basdif0  22895  tgval2  22898  ntreq0  23019  isclo2  23030  opnnei  23062  neiptopnei  23074  lmres  23242  ist1-3  23291  cmpcov2  23332  cmpsub  23342  is1stc2  23384  1stccn  23405  kgencn  23498  eltx  23510  txkgen  23594  fbun  23782  trfbas  23786  fbunfip  23811  trfil2  23829  isufil2  23850  fixufil  23864  hausflim  23923  txflf  23948  fclsopn  23956  alexsubALTlem3  23991  isclmp  25051  iscau3  25232  iscau4  25233  caucfil  25237  bcth3  25285  ovolgelb  25435  dyadmax  25553  itg2leub  25689  itg2cn  25718  plydivex  26259  vieta1  26274  lgseisenlem2  27341  pnt3  27577  nosepon  27631  nomaxmo  27664  nosupbnd1lem4  27677  conway  27767  eqscut2  27774  etasslt  27781  slerec  27787  bday1s  27802  cuteq1  27805  madebdaylemlrcut  27871  addsproplem4  27942  addsproplem6  27944  addsprop  27946  addsuniflem  27971  mulsuniflem  28118  onscutlt  28232  onsiso  28236  onsfi  28316  bdayn0p1  28327  addhalfcut  28416  tglowdim2ln  28672  axcontlem12  28997  elntg2  29007  numedglnl  29166  vtxd0nedgb  29511  wlkvtxedg  29666  pthd  29791  2pthdlem1  29952  clwlkclwwlk  30026  3pthdlem1  30188  frgrregord013  30419  grpoidinvlem3  30530  nmoubi  30796  lnon0  30822  adjsym  31857  nmopub  31932  nmfnleub  31949  cvbr2  32307  chpssati  32387  chrelat2i  32389  chrelat3  32395  mdsymlem8  32434  ralcom4f  32490  reuxfrdf  32514  n0nsnel  32539  uniinn0  32574  ssiun3  32582  disjnf  32594  disjorf  32603  disjunsn  32618  ac6sf2  32649  nn0min  32850  tosglblem  33005  archiabl  33229  1arithidom  33567  eulerpartlems  34466  eulerpartlemr  34480  eulerpartlemn  34487  ballotlem7  34642  bnj110  34963  bnj92  34967  bnj539  34996  bnj540  34997  bnj580  35018  bnj978  35054  bnj1047  35078  bnj1128  35095  bnj1417  35146  bnj1421  35147  bnj1312  35163  bnj1498  35166  onvf1od  35250  lfuhgr3  35263  subfacp1lem3  35325  cvmlift2lem1  35445  cvmlift2lem12  35457  satfv1  35506  fmlaomn0  35533  fmla0disjsuc  35541  fmlasucdisj  35542  untuni  35852  dfso3  35863  elintfv  35908  elpotr  35922  dfon2lem7  35930  dfon2lem9  35932  dfint3  36095  brlb  36098  filnetlem4  36524  bj-reabeq  37171  ctbssinf  37550  fvineqsneq  37556  pibt2  37561  phpreu  37744  ptrecube  37760  poimirlem1  37761  poimirlem25  37785  poimirlem26  37786  poimirlem27  37787  poimirlem30  37790  mblfinlem2  37798  ftc1anc  37841  inixp  37868  ac6gf  37872  heibor1lem  37949  heiborlem1  37951  iscrngo2  38137  ac6s3f  38311  ref5  38451  idinxpssinxp2  38456  n0elqs  38464  ineleq  38486  ssdmral  38503  refrelcosslem  38664  refrelcoss3  38665  lpssat  39212  lssat  39215  lcvbr2  39221  lcvbr3  39222  lfl1  39269  lub0N  39388  glb0N  39392  atlrelat1  39520  hlrelat2  39602  ispsubsp2  39945  pclclN  40090  cdleme25cv  40557  tendoeq2  40973  cdlemk35  41111  aks4d1p7  42276  sticksstones1  42339  indstrd  42386  supinf  42439  infdesc  42828  setindtrs  43209  unielss  43402  ssunib  43404  onsupmaxb  43423  onsupeqnmax  43431  cllem0  43749  ntrneixb  44278  gneispace  44317  expandral  44473  ismnuprim  44477  dfuniv2  44485  undisjrab  44489  zfregs2VD  45023  sswfaxreg  45170  dfac5prim  45173  permac8prim  45197  iindif2f  45346  ralfal  45347  disjinfi  45378  iuneqfzuz  45522  caucvgbf  45675  rexanuz2nf  45678  mccl  45786  limsupub  45890  limsuppnflem  45896  limsupre2lem  45910  lmbr3v  45931  liminfpnfuz  46002  xlimpnfxnegmnf2  46044  ioodvbdlimc1lem2  46118  ioodvbdlimc2lem  46120  dvnprodlem3  46134  fourierdlem103  46395  fourierdlem104  46396  sge0iunmpt  46604  meaiuninc3v  46670  hoidmvle  46786  issmff  46920  n0nsn2el  47213  r19.32  47286  2rexrsb  47290  cbvral2  47291  2reu3  47298  2reu8i  47301  otiunsndisjX  47467  0nelsetpreimafv  47578  dfgric2  48103  gpg5nbgrvtx03starlem1  48256  gpg5nbgrvtx03starlem2  48257  gpg5nbgrvtx03starlem3  48258  gpg5nbgrvtx13starlem1  48259  gpg5nbgrvtx13starlem2  48260  gpg5nbgrvtx13starlem3  48261  gpg5edgnedg  48318  copisnmnd  48357  lindslinindsimp1  48645  lindslinindsimp2  48651  snlindsntor  48659  ldepslinc  48697  iuneq0  49006  iinxp  49018  iscnrm3  49139  setrec1lem3  49876  aacllem  49988