Theorem ralbii 3108

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  dfral2  3113  ralinexa  3115  rexanali  3116  r19.26-3  3123  ralbiim  3124  2ralbii  3137  3ralbii  3139  4ralbii  3140  2ralbiim  3141  ralnex2  3142  nrexralim  3146  r19.26-2  3147  r19.23v  3189  r19.32v  3195  2ralor  3236  nelb  3238  cbvral2vw  3244  cbvral3vw  3246  ralrot3  3293  ralcom13  3294  sbralieALT  3339  cbvral2v  3353  cbvral3v  3355  ceqsralv  3490  ralxpxfr2d  3600  reu8  3691  2reuswap  3704  2reu5lem2  3714  2rmoswap  3719  rmoanim  3842  rmoanimALT  3843  dfdif3  4066  dfss5  4221  n0el  4312  ralnralall  4469  2reu4lem  4479  r19.12sn  4681  raldifsnb  4759  eqsn  4790  n0snor2el  4793  uni0b  4894  uni0c  4895  ssint  4924  iuniin  4964  iuneq2  4971  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  ssiinf  5013  iinab  5026  iinun2  5031  iindif1  5035  iindif2  5037  iinin2  5038  iinuni  5058  sspwuni  5060  iinpw  5066  disjor  5085  disjxun  5101  dftr3  5217  reusv3  5370  otiunsndisj  5497  ssrel2  5765  reliun  5797  xpiindi  5815  rexiunxp  5820  ralxpf  5826  rexxpf  5827  dfse2  6096  idrefALT  6107  asymref2  6111  rninxp  6172  dminxp  6173  cnviin  6284  cnvpo  6285  dfpo2  6294  dfse3  6334  frpoins2fg  6342  dffun9  6563  funcnv3  6604  fncnv  6607  fnres  6660  mptfnf  6668  fnopabg  6670  mptfng  6672  fint  6755  funimass4  6943  fndmdifeq0  7037  funconstss  7049  f1ompt  7105  idref  7143  fconstfv  7212  dff13f  7253  dff14b  7269  weniso  7358  fnssintima  7366  foov  7589  imaeqalov  7654  dfwe2  7774  tfis2f  7853  tfindes  7860  frxp  8125  ralxp3f  8136  frpoins3xpg  8139  frpoins3xp3g  8140  xpord2indlem  8146  xpord3inddlem  8153  soseq  8158  tz7.48lemOLD  8433  tz7.49  8437  oeordi  8578  naddcllem  8667  naddunif  8685  naddasslem2  8687  ixpeq2  8921  ixpin  8933  ixpiin  8934  boxriin  8950  findcard3  9256  fimax2g  9259  fissuni  9327  indexfi  9330  dfsup2  9417  sup0riota  9439  infcllem  9461  wemapsolem  9525  zfinf2  9624  oemapso  9664  ttrclresv  9699  zfregs2  9715  setinds  9731  setinds2f  9732  frins2f  9738  r1elss  9791  rankc1  9855  cp  9896  bnd2  9898  aceq1  10123  aceq2  10125  kmlem7  10162  kmlem12  10167  kmlem13  10168  kmlem15  10170  fin12  10418  ac6num  10484  ac6s2  10491  ac6sf  10494  ac6s4  10495  zorn2lem4  10504  zorn2lem6  10506  zorn2lem7  10507  zorng  10509  ttukeylem6  10519  brdom7disj  10537  brdom6disj  10538  fpwwe2  10655  fpwwe  10658  axgroth5  10836  axgroth4  10844  grothprim  10846  nqereu  10941  dfinfre  12223  infrenegsup  12225  xrsupsslem  13362  xrinfmsslem  13363  xrinfmss2  13366  fzshftral  13673  fsuppmapnn0ub  14062  mptnn0fsuppr  14066  hashgt12el  14490  hashgt12el2  14491  hashbc  14521  s3iunsndisj  15044  cotr2g  15052  rexfiuz  15438  clim0  15596  rpnnen2lem12  16316  gcdcllem1  16592  absproddvds  16710  coprmproddvdslem  16755  vdwmc2  17074  vdwlem13  17088  vdwnn  17093  xpscf  17654  mreacs  17749  acsfn  17750  acsfn1  17752  acsfn2  17754  dfinito2  18095  dftermo2  18096  ispos2  18406  lublecllem  18449  odulub  18496  oduglb  18498  posglbdg  18504  isnmnd  18843  gsumwspan  18958  smndex2dnrinv  19030  isnsg2  19282  oppgid  19486  oppgcntz  19494  efgval2  19854  iscyggen2  20011  iscyg3  20016  oppr1  20494  isnirred  20564  isdomn5  20875  lssne0  21138  iunocv  21897  islindf4  22054  pmatcollpw2lem  23005  isbasis2g  23176  basdif0  23181  tgval2  23184  ntreq0  23305  isclo2  23316  opnnei  23348  neiptopnei  23360  lmres  23528  ist1-3  23577  cmpcov2  23618  cmpsub  23628  is1stc2  23670  1stccn  23692  kgencn  23785  eltx  23797  txkgen  23881  fbun  24069  trfbas  24073  fbunfip  24098  trfil2  24116  isufil2  24137  fixufil  24151  hausflim  24210  txflf  24235  fclsopn  24243  alexsubALTlem3  24278  isclmp  25328  iscau3  25509  iscau4  25510  caucfil  25514  bcth3  25562  ovolgelb  25711  dyadmax  25829  itg2leub  25965  itg2cn  25994  plydivex  26530  vieta1  26547  lgseisenlem2  27615  pnt3  27851  nosepon  27904  nomaxmo  27937  nosupbnd1lem4  27950  conway  28047  eqcuts2  28054  etaslts  28061  lesrec  28067  bday1  28082  cuteq1  28085  madebdaylemlrcut  28167  addsproplem4  28240  addsproplem6  28242  addsprop  28244  addsuniflem  28269  mulsuniflem  28417  oncutlt  28532  oniso  28539  onsfi  28624  bdayn0p1  28637  addhalfcut  28727  tglowdim2ln  29002  axcontlem12  29435  elntg2  29445  numedglnl  29604  lfuhgr3  29610  vtxd0nedgb  29951  wlkvtxedg  30106  pthd  30237  2pthdlem1  30401  clwlkclwwlk  30475  3pthdlem1  30647  frgrregord013  30878  grpoidinvlem3  30990  nmoubi  31256  lnon0  31282  adjsym  32317  nmopub  32392  nmfnleub  32409  cvbr2  32767  chpssati  32847  chrelat2i  32849  chrelat3  32855  mdsymlem8  32894  ralcom4f  32946  reuxfrdf  32969  n0nsnel  32993  uniinn0  33029  ssiun3  33035  disjnf  33046  disjorf  33055  disjunsn  33070  ac6sf2  33098  nn0min  33294  tosglblem  33417  archiabl  33641  1arithidom  33950  eulerpartlems  34874  eulerpartlemr  34888  eulerpartlemn  34895  ballotlem7  35050  bnj110  35370  bnj92  35374  bnj539  35403  bnj540  35404  bnj580  35425  bnj978  35461  bnj1047  35485  bnj1128  35502  bnj1417  35553  bnj1421  35554  bnj1312  35570  bnj1498  35573  onvf1od  35707  subfacp1lem3  35764  cvmlift2lem1  35884  cvmlift2lem12  35896  satfv1  35945  fmlaomn0  35972  fmla0disjsuc  35980  fmlasucdisj  35981  untuni  36291  dfso3  36302  dffr5  36336  elintfv  36347  elpotr  36361  dfon2lem7  36369  dfon2lem9  36371  dfint3  36534  brlb  36537  dffr7  36538  filnetlem4  37003  axtco  37093  axtco1g  37098  regsfromregtco  37160  mh-infprim3bi  37170  bj-reabeq  37774  bj-axseprep  37822  ctbssinf  38163  fvineqsneq  38169  pibt2  38174  phpreu  38361  ptrecube  38372  poimirlem1  38373  poimirlem25  38397  poimirlem26  38398  poimirlem27  38399  poimirlem30  38402  mblfinlem2  38410  ftc1anc  38453  inixp  38481  ac6gf  38485  heibor1lem  38562  heiborlem1  38564  iscrngo2  38750  ac6s3f  38922  ref5  39070  idinxpssinxp2  39075  n0elqs  39083  ineleq  39105  ralrnmo  39112  ssdmral  39130  refrelcosslem  39303  refrelcoss3  39304  lpssat  39889  lssat  39892  lcvbr2  39898  lcvbr3  39899  lfl1  39946  lub0N  40065  glb0N  40069  atlrelat1  40197  hlrelat2  40279  ispsubsp2  40622  pclclN  40767  cdleme25cv  41234  tendoeq2  41650  cdlemk35  41788  aks4d1p7  42952  sticksstones1  43015  indstrd  43062  supinf  43112  infdesc  43492  setindtrs  43869  unielss  44062  ssunib  44064  onsupmaxb  44083  onsupeqnmax  44091  cllem0  44409  ntrneixb  44938  gneispace  44977  expandral  45117  ismnuprim  45121  dfuniv2  45129  undisjrab  45133  zfregs2VD  45666  sswfaxreg  45813  dfac5prim  45816  permac8prim  45840  iindif2f  45995  ralfal  45996  disjinfi  46027  iuneqfzuz  46168  caucvgbf  46320  rexanuz2nf  46323  mccl  46431  limsupub  46535  limsuppnflem  46541  limsupre2lem  46555  lmbr3v  46576  liminfpnfuz  46647  xlimpnfxnegmnf2  46689  ioodvbdlimc1lem2  46763  ioodvbdlimc2lem  46765  dvnprodlem3  46779  fourierdlem103  47040  fourierdlem104  47041  sge0iunmpt  47249  meaiuninc3v  47315  hoidmvle  47431  issmff  47565  n0nsn2el  47916  r19.32  47989  2rexrsb  47993  cbvral2  47994  2reu3  48001  2reu8i  48004  otiunsndisjX  48170  0nelsetpreimafv  48293  dfgric2  48834  gpg5nbgrvtx03starlem1  48987  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx03starlem3  48989  gpg5nbgrvtx13starlem1  48990  gpg5nbgrvtx13starlem2  48991  gpg5nbgrvtx13starlem3  48992  gpg5edgnedg  49049  copisnmnd  49087  lindslinindsimp1  49390  lindslinindsimp2  49396  snlindsntor  49404  ldepslinc  49442  iuneq0  49750  iinxp  49762  iscnrm3  49881  setrec1lem3  50618  ralsbii  50733  ralseubii  50765  aacllem  50775