Theorem ralbii 3075

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  dfral2  3080  ralinexa  3082  rexanali  3083  r19.26-3  3090  ralbiim  3091  2ralbii  3104  3ralbii  3106  4ralbii  3107  2ralbiim  3108  ralnex2  3109  nrexralim  3113  r19.26-2  3114  r19.23v  3156  r19.32v  3162  2ralor  3203  nelb  3205  cbvral2vw  3211  cbvral3vw  3213  ralrot3  3260  ralcom13  3261  sbralieALT  3316  cbvral2v  3331  cbvral3v  3333  ceqsralv  3477  ralxpxfr2d  3601  reu8  3693  2reuswap  3706  2reu5lem2  3716  2rmoswap  3721  rmoanim  3846  rmoanimALT  3847  dfdif3  4068  dfss5  4226  n0el  4315  ralnralall  4466  2reu4lem  4473  r19.12sn  4672  raldifsnb  4747  eqsn  4780  n0snor2el  4784  uni0b  4884  uni0c  4885  ssint  4914  iuniin  4954  iuneq2  4961  iunssf  4993  iunss  4994  ssiinf  5003  iinab  5017  iinun2  5022  iindif1  5024  iindif2  5026  iinin2  5027  iinuni  5047  sspwuni  5049  iinpw  5055  disjor  5074  disjxun  5090  dftr3  5204  reusv3  5344  otiunsndisj  5463  ssrel2  5728  reliun  5759  xpiindi  5778  rexiunxp  5783  ralxpf  5789  rexxpf  5790  dfse2  6051  idrefALT  6062  asymref2  6066  rninxp  6128  dminxp  6129  cnviin  6234  cnvpo  6235  dfpo2  6244  dfse3  6284  frpoins2fg  6292  dffun9  6511  funcnv3  6552  fncnv  6555  fnres  6609  mptfnf  6617  fnopabg  6619  mptfng  6621  fint  6703  funimass4  6887  fndmdifeq0  6978  funconstss  6990  f1ompt  7045  idref  7080  fconstfv  7148  dff13f  7192  dff14b  7208  weniso  7291  fnssintima  7299  foov  7523  imaeqalov  7588  dfwe2  7710  tfis2f  7789  tfindes  7796  frxp  8059  ralxp3f  8070  frpoins3xpg  8073  frpoins3xp3g  8074  xpord2indlem  8080  xpord3inddlem  8087  soseq  8092  tz7.48lem  8363  tz7.49  8367  oeordi  8505  naddcllem  8594  naddunif  8611  naddasslem2  8613  ixpeq2  8838  ixpin  8850  ixpiin  8851  boxriin  8867  findcard3  9172  fimax2g  9175  fissuni  9247  indexfi  9250  dfsup2  9334  sup0riota  9356  infcllem  9378  wemapsolem  9442  zfinf2  9538  oemapso  9578  ttrclresv  9613  zfregs2  9629  frins2f  9649  r1elss  9702  rankc1  9766  cp  9787  bnd2  9789  aceq1  10011  aceq2  10013  kmlem7  10051  kmlem12  10056  kmlem13  10057  kmlem15  10059  fin12  10307  ac6num  10373  ac6s2  10380  ac6sf  10383  ac6s4  10384  zorn2lem4  10393  zorn2lem6  10395  zorn2lem7  10396  zorng  10398  ttukeylem6  10408  brdom7disj  10425  brdom6disj  10426  fpwwe2  10537  fpwwe  10540  axgroth5  10718  axgroth4  10726  grothprim  10728  nqereu  10823  dfinfre  12106  infrenegsup  12108  xrsupsslem  13209  xrinfmsslem  13210  xrinfmss2  13213  fzshftral  13518  fsuppmapnn0ub  13902  mptnn0fsuppr  13906  hashgt12el  14329  hashgt12el2  14330  hashbc  14360  s3iunsndisj  14875  cotr2g  14883  rexfiuz  15255  clim0  15413  rpnnen2lem12  16134  gcdcllem1  16410  absproddvds  16528  coprmproddvdslem  16573  vdwmc2  16891  vdwlem13  16905  vdwnn  16910  xpscf  17469  mreacs  17564  acsfn  17565  acsfn1  17567  acsfn2  17569  dfinito2  17910  dftermo2  17911  ispos2  18221  lublecllem  18264  odulub  18311  oduglb  18313  posglbdg  18319  isnmnd  18612  gsumwspan  18720  smndex2dnrinv  18789  isnsg2  19035  oppgid  19235  oppgcntz  19243  efgval2  19603  iscyggen2  19760  iscyg3  19765  oppr1  20235  isnirred  20305  isdomn5  20595  isdomn2OLD  20597  lssne0  20854  iunocv  21588  islindf4  21745  pmatcollpw2lem  22662  isbasis2g  22833  basdif0  22838  tgval2  22841  ntreq0  22962  isclo2  22973  opnnei  23005  neiptopnei  23017  lmres  23185  ist1-3  23234  cmpcov2  23275  cmpsub  23285  is1stc2  23327  1stccn  23348  kgencn  23441  eltx  23453  txkgen  23537  fbun  23725  trfbas  23729  fbunfip  23754  trfil2  23772  isufil2  23793  fixufil  23807  hausflim  23866  txflf  23891  fclsopn  23899  alexsubALTlem3  23934  isclmp  24995  iscau3  25176  iscau4  25177  caucfil  25181  bcth3  25229  ovolgelb  25379  dyadmax  25497  itg2leub  25633  itg2cn  25662  plydivex  26203  vieta1  26218  lgseisenlem2  27285  pnt3  27521  nosepon  27575  nomaxmo  27608  nosupbnd1lem4  27621  conway  27710  eqscut2  27717  etasslt  27724  slerec  27730  bday1s  27745  cuteq1  27748  madebdaylemlrcut  27813  addsproplem4  27884  addsproplem6  27886  addsprop  27888  addsuniflem  27913  mulsuniflem  28057  onscutlt  28170  onsiso  28174  onsfi  28252  bdayn0p1  28263  addhalfcut  28347  tglowdim2ln  28596  axcontlem12  28920  elntg2  28930  numedglnl  29089  vtxd0nedgb  29434  wlkvtxedg  29589  pthd  29714  2pthdlem1  29875  clwlkclwwlk  29946  3pthdlem1  30108  frgrregord013  30339  grpoidinvlem3  30450  nmoubi  30716  lnon0  30742  adjsym  31777  nmopub  31852  nmfnleub  31869  cvbr2  32227  chpssati  32307  chrelat2i  32309  chrelat3  32315  mdsymlem8  32354  ralcom4f  32411  reuxfrdf  32435  n0nsnel  32459  uniinn0  32494  ssiun3  32502  disjnf  32514  disjorf  32523  disjunsn  32538  ac6sf2  32566  nn0min  32765  tosglblem  32916  archiabl  33140  1arithidom  33474  eulerpartlems  34328  eulerpartlemr  34342  eulerpartlemn  34349  ballotlem7  34504  bnj110  34825  bnj92  34829  bnj539  34858  bnj540  34859  bnj580  34880  bnj978  34916  bnj1047  34940  bnj1128  34957  bnj1417  35008  bnj1421  35009  bnj1312  35025  bnj1498  35028  onvf1od  35084  lfuhgr3  35097  subfacp1lem3  35159  cvmlift2lem1  35279  cvmlift2lem12  35291  satfv1  35340  fmlaomn0  35367  fmla0disjsuc  35375  fmlasucdisj  35376  untuni  35686  dfso3  35697  elintfv  35742  setinds  35756  setinds2f  35757  elpotr  35759  dfon2lem7  35767  dfon2lem9  35769  dfint3  35930  brlb  35933  filnetlem4  36359  bj-reabeq  37005  ctbssinf  37384  fvineqsneq  37390  pibt2  37395  phpreu  37588  ptrecube  37604  poimirlem1  37605  poimirlem25  37629  poimirlem26  37630  poimirlem27  37631  poimirlem30  37634  mblfinlem2  37642  ftc1anc  37685  inixp  37712  ac6gf  37716  heibor1lem  37793  heiborlem1  37795  iscrngo2  37981  ac6s3f  38155  ref5  38291  idinxpssinxp2  38296  n0elqs  38304  ineleq  38326  refrelcosslem  38443  refrelcoss3  38444  lpssat  38996  lssat  38999  lcvbr2  39005  lcvbr3  39006  lfl1  39053  lub0N  39172  glb0N  39176  atlrelat1  39304  hlrelat2  39386  ispsubsp2  39729  pclclN  39874  cdleme25cv  40341  tendoeq2  40757  cdlemk35  40895  aks4d1p7  42060  sticksstones1  42123  indstrd  42170  supinf  42219  infdesc  42620  setindtrs  43002  unielss  43195  ssunib  43197  onsupmaxb  43216  onsupeqnmax  43224  cllem0  43543  ntrneixb  44072  gneispace  44111  expandral  44267  ismnuprim  44271  dfuniv2  44279  undisjrab  44283  zfregs2VD  44818  sswfaxreg  44965  dfac5prim  44968  permac8prim  44992  iindif2f  45142  ralfal  45143  disjinfi  45174  iuneqfzuz  45319  caucvgbf  45472  rexanuz2nf  45475  mccl  45583  limsupub  45689  limsuppnflem  45695  limsupre2lem  45709  lmbr3v  45730  liminfpnfuz  45801  xlimpnfxnegmnf2  45843  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnprodlem3  45933  fourierdlem103  46194  fourierdlem104  46195  sge0iunmpt  46403  meaiuninc3v  46469  hoidmvle  46585  issmff  46719  n0nsn2el  47013  r19.32  47086  2rexrsb  47090  cbvral2  47091  2reu3  47098  2reu8i  47101  otiunsndisjX  47267  0nelsetpreimafv  47378  dfgric2  47903  gpg5nbgrvtx03starlem1  48056  gpg5nbgrvtx03starlem2  48057  gpg5nbgrvtx03starlem3  48058  gpg5nbgrvtx13starlem1  48059  gpg5nbgrvtx13starlem2  48060  gpg5nbgrvtx13starlem3  48061  gpg5edgnedg  48118  copisnmnd  48157  lindslinindsimp1  48446  lindslinindsimp2  48452  snlindsntor  48460  ldepslinc  48498  iuneq0  48807  iinxp  48819  iscnrm3  48940  setrec1lem3  49678  aacllem  49790