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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∀wral 3061

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 3062

This theorem is referenced by:  dfral2  3099  ralinexa  3101  rexanali  3102  rexbiOLD  3105  r19.26-3  3112  ralbiim  3113  2ralbii  3128  3ralbii  3130  4ralbii  3131  2ralbiim  3132  ralnex2  3133  nrexralim  3137  r19.26-2  3138  r19.23v  3183  r19.32v  3192  2ralor  3231  nelb  3234  nelbOLD  3235  cbvral2vw  3241  cbvral3vw  3243  ralrot3  3293  ralcom13  3294  ralcom13OLD  3295  sbralieALT  3359  cbvral2v  3368  cbvral3v  3370  moelOLD  3405  ceqsralv  3522  ralxpxfr2d  3646  reu8  3739  2reuswap  3752  2reu5lem2  3762  2rmoswap  3767  rmoanim  3894  rmoanimALT  3895  dfdif3  4117  dfss5  4275  n0el  4364  ralnralall  4515  2reu4lem  4522  r19.12sn  4720  raldifsnb  4796  eqsn  4829  n0snor2el  4833  uni0b  4933  uni0c  4934  ssint  4964  iuniin  5004  iuneq2  5011  iunssf  5044  iunss  5045  ssiinf  5054  iinab  5068  iinun2  5073  iindif1  5075  iindif2  5077  iinin2  5078  iinuni  5098  sspwuni  5100  iinpw  5106  disjor  5125  disjxun  5141  dftr3  5265  reusv3  5405  otiunsndisj  5525  ssrel2  5795  reliun  5826  xpiindi  5846  rexiunxp  5851  ralxpf  5857  rexxpf  5858  dfse2  6118  idrefALT  6131  asymref2  6137  rninxp  6199  dminxp  6200  cnviin  6306  cnvpo  6307  dfpo2  6316  dfse3  6357  frpoins2fg  6365  wfis2fgOLD  6378  dffun9  6595  funcnv3  6636  fncnv  6639  fnres  6695  mptfnf  6703  fnopabg  6705  mptfng  6707  fint  6787  funimass4  6973  fndmdifeq0  7064  funconstss  7076  f1ompt  7131  idref  7166  fconstfv  7232  dff13f  7276  dff14b  7291  weniso  7374  fnssintima  7382  foov  7607  imaeqalov  7672  dfwe2  7794  tfis2f  7877  tfindes  7884  frxp  8151  ralxp3f  8162  frpoins3xpg  8165  frpoins3xp3g  8166  xpord2indlem  8172  xpord3inddlem  8179  soseq  8184  dfwrecsOLD  8338  tz7.48lem  8481  tz7.49  8485  oeordi  8625  naddcllem  8714  naddunif  8731  naddasslem2  8733  ixpeq2  8951  ixpin  8963  ixpiin  8964  boxriin  8980  findcard3  9318  findcard3OLD  9319  fimax2g  9322  fissuni  9397  indexfi  9400  dfsup2  9484  sup0riota  9505  infcllem  9527  wemapsolem  9590  zfinf2  9682  oemapso  9722  ttrclresv  9757  zfregs2  9773  frins2f  9793  r1elss  9846  rankc1  9910  cp  9931  bnd2  9933  aceq1  10157  aceq2  10159  kmlem7  10197  kmlem12  10202  kmlem13  10203  kmlem15  10205  fin12  10453  ac6num  10519  ac6s2  10526  ac6sf  10529  ac6s4  10530  zorn2lem4  10539  zorn2lem6  10541  zorn2lem7  10542  zorng  10544  ttukeylem6  10554  brdom7disj  10571  brdom6disj  10572  fpwwe2  10683  fpwwe  10686  axgroth5  10864  axgroth4  10872  grothprim  10874  nqereu  10969  dfinfre  12249  infrenegsup  12251  xrsupsslem  13349  xrinfmsslem  13350  xrinfmss2  13353  fzshftral  13655  fsuppmapnn0ub  14036  mptnn0fsuppr  14040  hashgt12el  14461  hashgt12el2  14462  hashbc  14492  s3iunsndisj  15007  cotr2g  15015  rexfiuz  15386  clim0  15542  rpnnen2lem12  16261  gcdcllem1  16536  absproddvds  16654  coprmproddvdslem  16699  vdwmc2  17017  vdwlem13  17031  vdwnn  17036  xpscf  17610  mreacs  17701  acsfn  17702  acsfn1  17704  acsfn2  17706  dfinito2  18048  dftermo2  18049  ispos2  18361  lublecllem  18405  odulub  18452  oduglb  18454  posglbdg  18460  isnmnd  18751  gsumwspan  18859  smndex2dnrinv  18928  isnsg2  19174  oppgid  19375  oppgcntz  19383  efgval2  19742  iscyggen2  19899  iscyg3  19904  oppr1  20350  isnirred  20420  isdomn5  20710  isdomn2OLD  20712  lssne0  20949  iunocv  21699  islindf4  21858  pmatcollpw2lem  22783  isbasis2g  22955  basdif0  22960  tgval2  22963  ntreq0  23085  isclo2  23096  opnnei  23128  neiptopnei  23140  lmres  23308  ist1-3  23357  cmpcov2  23398  cmpsub  23408  is1stc2  23450  1stccn  23471  kgencn  23564  eltx  23576  txkgen  23660  fbun  23848  trfbas  23852  fbunfip  23877  trfil2  23895  isufil2  23916  fixufil  23930  hausflim  23989  txflf  24014  fclsopn  24022  alexsubALTlem3  24057  isclmp  25130  iscau3  25312  iscau4  25313  caucfil  25317  bcth3  25365  ovolgelb  25515  dyadmax  25633  itg2leub  25769  itg2cn  25798  plydivex  26339  vieta1  26354  lgseisenlem2  27420  pnt3  27656  nosepon  27710  nomaxmo  27743  nosupbnd1lem4  27756  conway  27844  eqscut2  27851  etasslt  27858  slerec  27864  bday1s  27876  cuteq1  27878  madebdaylemlrcut  27937  addsproplem4  28005  addsproplem6  28007  addsprop  28009  addsuniflem  28034  mulsuniflem  28175  halfcut  28416  addhalfcut  28419  tglowdim2ln  28659  axcontlem12  28990  elntg2  29000  numedglnl  29161  vtxd0nedgb  29506  wlkvtxedg  29662  pthd  29789  2pthdlem1  29950  clwlkclwwlk  30021  3pthdlem1  30183  frgrregord013  30414  grpoidinvlem3  30525  nmoubi  30791  lnon0  30817  adjsym  31852  nmopub  31927  nmfnleub  31944  cvbr2  32302  chpssati  32382  chrelat2i  32384  chrelat3  32390  mdsymlem8  32429  ralcom4f  32486  reuxfrdf  32510  n0nsnel  32534  uniinn0  32563  ssiun3  32571  disjnf  32583  disjorf  32592  disjunsn  32607  ac6sf2  32634  nn0min  32822  tosglblem  32964  archiabl  33205  1arithidom  33565  eulerpartlems  34362  eulerpartlemr  34376  eulerpartlemn  34383  ballotlem7  34538  bnj110  34872  bnj92  34876  bnj539  34905  bnj540  34906  bnj580  34927  bnj978  34963  bnj1047  34987  bnj1128  35004  bnj1417  35055  bnj1421  35056  bnj1312  35072  bnj1498  35075  lfuhgr3  35125  subfacp1lem3  35187  cvmlift2lem1  35307  cvmlift2lem12  35319  satfv1  35368  fmlaomn0  35395  fmla0disjsuc  35403  fmlasucdisj  35404  untuni  35709  dfso3  35720  elintfv  35765  setinds  35779  setinds2f  35780  elpotr  35782  dfon2lem7  35790  dfon2lem9  35792  dfint3  35953  brlb  35956  filnetlem4  36382  bj-reabeq  37028  ctbssinf  37407  fvineqsneq  37413  pibt2  37418  phpreu  37611  ptrecube  37627  poimirlem1  37628  poimirlem25  37652  poimirlem26  37653  poimirlem27  37654  poimirlem30  37657  mblfinlem2  37665  ftc1anc  37708  inixp  37735  ac6gf  37739  heibor1lem  37816  heiborlem1  37818  iscrngo2  38004  ac6s3f  38178  ref5  38314  idinxpssinxp2  38319  n0elqs  38327  ineleq  38355  refrelcosslem  38463  refrelcoss3  38464  lpssat  39014  lssat  39017  lcvbr2  39023  lcvbr3  39024  lfl1  39071  lub0N  39190  glb0N  39194  atlrelat1  39322  hlrelat2  39405  ispsubsp2  39748  pclclN  39893  cdleme25cv  40360  tendoeq2  40776  cdlemk35  40914  aks4d1p7  42084  sticksstones1  42147  indstrd  42194  supinf  42283  infdesc  42653  setindtrs  43037  unielss  43230  ssunib  43232  onsupmaxb  43251  onsupeqnmax  43259  cllem0  43579  ntrneixb  44108  gneispace  44147  expandral  44309  ismnuprim  44313  dfuniv2  44321  undisjrab  44325  zfregs2VD  44861  sswfaxreg  45004  dfac5prim  45007  iindif2f  45165  ralfal  45166  disjinfi  45197  iuneqfzuz  45346  caucvgbf  45500  rexanuz2nf  45503  mccl  45613  limsupub  45719  limsuppnflem  45725  limsupre2lem  45739  lmbr3v  45760  liminfpnfuz  45831  xlimpnfxnegmnf2  45873  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem3  45963  fourierdlem103  46224  fourierdlem104  46225  sge0iunmpt  46433  meaiuninc3v  46499  hoidmvle  46615  issmff  46749  n0nsn2el  47037  r19.32  47110  2rexrsb  47114  cbvral2  47115  2reu3  47122  2reu8i  47125  otiunsndisjX  47291  0nelsetpreimafv  47377  dfgric2  47884  gpg5nbgrvtx03starlem1  48024  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx03starlem3  48026  gpg5nbgrvtx13starlem1  48027  gpg5nbgrvtx13starlem2  48028  gpg5nbgrvtx13starlem3  48029  copisnmnd  48085  lindslinindsimp1  48374  lindslinindsimp2  48380  snlindsntor  48388  ldepslinc  48426  iscnrm3  48849  setrec1lem3  49208  aacllem  49320