Theorem ralbii 3093

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

Syntax hints:   ↔ wb 205   ∈ wcel 2107  ∀wral 3065

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

This theorem depends on definitions:  df-bi 206  df-ral 3070

This theorem is referenced by:  2ralbii  3094  r19.26-2  3097  r19.26-3  3098  ralbiim  3100  2ralbiim  3101  dfral2  3169  rexbiOLD  3175  ralnex2  3190  ralinexa  3192  rexanali  3193  nrexralim  3194  nelb  3196  nelbOLD  3197  r19.23v  3209  r19.32v  3271  ralcom13  3287  ralrot3  3289  2ralor  3297  moelOLD  3360  cbvral2vw  3397  cbvral3vw  3399  cbvral2v  3400  cbvral3v  3402  sbralie  3407  ceqsralv  3470  ralxpxfr2d  3577  reu8  3669  2reuswap  3682  2reu5lem2  3692  2rmoswap  3697  rmoanim  3828  rmoanimALT  3829  dfss5  4199  n0el  4296  ralnralall  4450  2reu4lem  4457  r19.12sn  4657  raldifsnb  4730  eqsn  4763  n0snor2el  4765  uni0b  4868  uni0c  4869  ssint  4896  iuniin  4937  iuneq2  4944  iunssf  4975  iunss  4976  ssiinf  4985  iinab  4998  iinun2  5003  iindif1  5005  iindif2  5007  iinin2  5008  iinuni  5028  sspwuni  5030  iinpw  5036  disjor  5055  disjxun  5073  dftr3  5196  reusv3  5329  otiunsndisj  5435  ssrel2  5697  reliun  5728  xpiindi  5747  rexiunxp  5752  ralxpf  5758  rexxpf  5759  dfse2  6011  idrefALT  6023  asymref2  6027  rninxp  6087  dminxp  6088  cnviin  6193  cnvpo  6194  dfpo2  6203  dfse3  6243  frpoins2fg  6251  wfis2fgOLD  6264  dffun9  6470  funcnv3  6511  fncnv  6514  fnres  6568  mptfnf  6577  fnopabg  6579  mptfng  6581  fint  6662  funimass4  6843  fndmdifeq0  6930  funconstss  6942  f1ompt  6994  idref  7027  fconstfv  7097  dff13f  7138  dff14b  7153  weniso  7234  foov  7455  dfwe2  7633  tfis2f  7711  tfindes  7718  frxp  7976  dfwrecsOLD  8138  tz7.48lem  8281  tz7.49  8285  oeordi  8427  ixpeq2  8708  ixpin  8720  ixpiin  8721  boxriin  8737  findcard3  9066  fimax2g  9069  fissuni  9133  indexfi  9136  dfsup2  9212  sup0riota  9233  infcllem  9255  wemapsolem  9318  zfinf2  9409  oemapso  9449  ttrclresv  9484  zfregs2  9500  frins2f  9520  r1elss  9573  rankc1  9637  cp  9658  bnd2  9660  aceq1  9882  aceq2  9884  kmlem7  9921  kmlem12  9926  kmlem13  9927  kmlem15  9929  fin12  10178  ac6num  10244  ac6s2  10251  ac6sf  10254  ac6s4  10255  zorn2lem4  10264  zorn2lem6  10266  zorn2lem7  10267  zorng  10269  ttukeylem6  10279  brdom7disj  10296  brdom6disj  10297  fpwwe2  10408  fpwwe  10411  axgroth5  10589  axgroth4  10597  grothprim  10599  nqereu  10694  dfinfre  11965  infrenegsup  11967  xrsupsslem  13050  xrinfmsslem  13051  xrinfmss2  13054  fzshftral  13353  fsuppmapnn0ub  13724  mptnn0fsuppr  13728  hashgt12el  14146  hashgt12el2  14147  hashbc  14174  s3iunsndisj  14688  cotr2g  14696  rexfiuz  15068  clim0  15224  rpnnen2lem12  15943  gcdcllem1  16215  absproddvds  16331  coprmproddvdslem  16376  vdwmc2  16689  vdwlem13  16703  vdwnn  16708  xpscf  17285  mreacs  17376  acsfn  17377  acsfn1  17379  acsfn2  17381  dfinito2  17727  dftermo2  17728  ispos2  18042  lublecllem  18087  odulub  18134  oduglb  18136  posglbdg  18142  isnmnd  18398  gsumwspan  18494  smndex2dnrinv  18563  isnsg2  18793  oppgid  18972  oppgcntz  18980  efgval2  19339  iscyggen2  19490  iscyg3  19495  oppr1  19885  isnirred  19951  lssne0  20221  isdomn2  20579  iunocv  20895  islindf4  21054  pmatcollpw2lem  21935  isbasis2g  22107  basdif0  22112  tgval2  22115  ntreq0  22237  isclo2  22248  opnnei  22280  neiptopnei  22292  lmres  22460  ist1-3  22509  cmpcov2  22550  cmpsub  22560  is1stc2  22602  1stccn  22623  kgencn  22716  eltx  22728  txkgen  22812  fbun  23000  trfbas  23004  fbunfip  23029  trfil2  23047  isufil2  23068  fixufil  23082  hausflim  23141  txflf  23166  fclsopn  23174  alexsubALTlem3  23209  isclmp  24269  iscau3  24451  iscau4  24452  caucfil  24456  bcth3  24504  ovolgelb  24653  dyadmax  24771  itg2leub  24908  itg2cn  24937  plydivex  25466  vieta1  25481  lgseisenlem2  26533  pnt3  26769  tglowdim2ln  27021  axcontlem12  27352  elntg2  27362  numedglnl  27523  vtxd0nedgb  27864  wlkvtxedg  28020  pthd  28146  2pthdlem1  28304  clwlkclwwlk  28375  3pthdlem1  28537  frgrregord013  28768  grpoidinvlem3  28877  nmoubi  29143  lnon0  29169  adjsym  30204  nmopub  30279  nmfnleub  30296  cvbr2  30654  chpssati  30734  chrelat2i  30736  chrelat3  30742  mdsymlem8  30781  nelbOLDOLD  30826  ralcom4f  30827  reuxfrdf  30848  uniinn0  30899  ssiun3  30907  disjnf  30918  disjorf  30927  disjunsn  30942  ac6sf2  30969  nn0min  31143  tosglblem  31261  archiabl  31461  eulerpartlems  32336  eulerpartlemr  32350  eulerpartlemn  32357  ballotlem7  32511  bnj110  32847  bnj92  32851  bnj539  32880  bnj540  32881  bnj580  32902  bnj978  32938  bnj1047  32962  bnj1128  32979  bnj1417  33030  bnj1421  33031  bnj1312  33047  bnj1498  33050  lfuhgr3  33090  subfacp1lem3  33153  cvmlift2lem1  33273  cvmlift2lem12  33285  satfv1  33334  fmlaomn0  33361  fmla0disjsuc  33369  fmlasucdisj  33370  untuni  33659  dfso3  33673  fnssintima  33685  ralxp3f  33694  elintfv  33747  setinds  33763  setinds2f  33764  elpotr  33766  dfon2lem7  33774  dfon2lem9  33776  frpoins3xpg  33796  frpoins3xp3g  33797  xpord2ind  33803  xpord3ind  33809  soseq  33812  naddcllem  33840  nosepon  33877  nomaxmo  33910  nosupbnd1lem4  33923  conway  34002  eqscut2  34009  etasslt  34016  slerec  34022  bday1s  34034  madebdaylemlrcut  34088  dfint3  34263  brlb  34266  filnetlem4  34579  bj-reabeq  35226  ctbssinf  35586  fvineqsneq  35592  pibt2  35597  phpreu  35770  ptrecube  35786  poimirlem1  35787  poimirlem25  35811  poimirlem26  35812  poimirlem27  35813  poimirlem30  35816  mblfinlem2  35824  ftc1anc  35867  inixp  35895  ac6gf  35899  heibor1lem  35976  heiborlem1  35978  iscrngo2  36164  ac6s3f  36338  3ralbii  36396  idinxpssinxp2  36460  n0elqs  36468  ineleq  36493  refrelcosslem  36587  refrelcoss3  36588  lpssat  37034  lssat  37037  lcvbr2  37043  lcvbr3  37044  lfl1  37091  lub0N  37210  glb0N  37214  atlrelat1  37342  hlrelat2  37424  ispsubsp2  37767  pclclN  37912  cdleme25cv  38379  tendoeq2  38795  cdlemk35  38933  aks4d1p7  40098  sticksstones1  40109  isdomn5  40178  infdesc  40487  setindtrs  40854  cllem0  41180  ss2iundf  41274  ntrneixb  41712  gneispace  41751  expandral  41915  ismnuprim  41919  dfuniv2  41927  undisjrab  41931  zfregs2VD  42468  disjinfi  42738  iuneqfzuz  42881  mccl  43146  limsupub  43252  limsuppnflem  43258  limsupre2lem  43272  lmbr3v  43293  liminfpnfuz  43364  xlimpnfxnegmnf2  43406  ioodvbdlimc1lem2  43480  ioodvbdlimc2lem  43482  dvnprodlem3  43496  fourierdlem103  43757  fourierdlem104  43758  sge0iunmpt  43963  meaiuninc3v  44029  hoidmvle  44145  issmff  44279  r19.32  44601  2rexrsb  44605  cbvral2  44606  2reu3  44613  2reu8i  44616  otiunsndisjX  44782  0nelsetpreimafv  44853  copisnmnd  45374  lindslinindsimp1  45809  lindslinindsimp2  45815  snlindsntor  45823  ldepslinc  45861  iscnrm3  46257  setrec1lem3  46406  aacllem  46516