Theorem ralbii 3094

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 3062

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 3063

This theorem is referenced by:  dfral2  3100  ralinexa  3102  rexanali  3103  rexbiOLD  3106  r19.26-3  3113  ralbiim  3114  2ralbii  3129  3ralbii  3131  4ralbii  3132  2ralbiim  3133  ralnex2  3134  nrexralim  3138  r19.26-2  3139  r19.23v  3183  r19.32v  3192  2ralor  3229  nelb  3232  nelbOLD  3233  cbvral2vw  3239  cbvral3vw  3241  ralrot3  3291  ralcom13  3292  ralcom13OLD  3293  sbralieALT  3356  cbvral2v  3365  cbvral3v  3367  moelOLD  3402  ceqsralv  3514  ralxpxfr2d  3634  reu8  3729  2reuswap  3742  2reu5lem2  3752  2rmoswap  3757  rmoanim  3888  rmoanimALT  3889  dfss5  4264  n0el  4361  ralnralall  4518  2reu4lem  4525  r19.12sn  4724  raldifsnb  4799  eqsn  4832  n0snor2el  4834  uni0b  4937  uni0c  4938  ssint  4968  iuniin  5009  iuneq2  5016  iunssf  5047  iunss  5048  ssiinf  5057  iinab  5071  iinun2  5076  iindif1  5078  iindif2  5080  iinin2  5081  iinuni  5101  sspwuni  5103  iinpw  5109  disjor  5128  disjxun  5146  dftr3  5271  reusv3  5403  otiunsndisj  5520  ssrel2  5784  reliun  5815  xpiindi  5834  rexiunxp  5839  ralxpf  5845  rexxpf  5846  dfse2  6097  idrefALT  6110  asymref2  6116  rninxp  6176  dminxp  6177  cnviin  6283  cnvpo  6284  dfpo2  6293  dfse3  6335  frpoins2fg  6343  wfis2fgOLD  6356  dffun9  6575  funcnv3  6616  fncnv  6619  fnres  6675  mptfnf  6683  fnopabg  6685  mptfng  6687  fint  6768  funimass4  6954  fndmdifeq0  7043  funconstss  7055  f1ompt  7108  idref  7141  fconstfv  7211  dff13f  7252  dff14b  7267  weniso  7348  fnssintima  7356  foov  7578  imaeqalov  7643  dfwe2  7758  tfis2f  7842  tfindes  7849  frxp  8109  ralxp3f  8120  frpoins3xpg  8123  frpoins3xp3g  8124  xpord2indlem  8130  xpord3inddlem  8137  soseq  8142  dfwrecsOLD  8295  tz7.48lem  8438  tz7.49  8442  oeordi  8584  naddcllem  8672  naddunif  8689  naddasslem2  8691  ixpeq2  8902  ixpin  8914  ixpiin  8915  boxriin  8931  findcard3  9282  findcard3OLD  9283  fimax2g  9286  fissuni  9354  indexfi  9357  dfsup2  9436  sup0riota  9457  infcllem  9479  wemapsolem  9542  zfinf2  9634  oemapso  9674  ttrclresv  9709  zfregs2  9725  frins2f  9745  r1elss  9798  rankc1  9862  cp  9883  bnd2  9885  aceq1  10109  aceq2  10111  kmlem7  10148  kmlem12  10153  kmlem13  10154  kmlem15  10156  fin12  10405  ac6num  10471  ac6s2  10478  ac6sf  10481  ac6s4  10482  zorn2lem4  10491  zorn2lem6  10493  zorn2lem7  10494  zorng  10496  ttukeylem6  10506  brdom7disj  10523  brdom6disj  10524  fpwwe2  10635  fpwwe  10638  axgroth5  10816  axgroth4  10824  grothprim  10826  nqereu  10921  dfinfre  12192  infrenegsup  12194  xrsupsslem  13283  xrinfmsslem  13284  xrinfmss2  13287  fzshftral  13586  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  hashgt12el  14379  hashgt12el2  14380  hashbc  14409  s3iunsndisj  14912  cotr2g  14920  rexfiuz  15291  clim0  15447  rpnnen2lem12  16165  gcdcllem1  16437  absproddvds  16551  coprmproddvdslem  16596  vdwmc2  16909  vdwlem13  16923  vdwnn  16928  xpscf  17508  mreacs  17599  acsfn  17600  acsfn1  17602  acsfn2  17604  dfinito2  17950  dftermo2  17951  ispos2  18265  lublecllem  18310  odulub  18357  oduglb  18359  posglbdg  18365  isnmnd  18626  gsumwspan  18724  smndex2dnrinv  18793  isnsg2  19031  oppgid  19218  oppgcntz  19226  efgval2  19587  iscyggen2  19744  iscyg3  19749  oppr1  20157  isnirred  20227  lssne0  20554  isdomn2  20908  isdomn5  20910  iunocv  21226  islindf4  21385  pmatcollpw2lem  22271  isbasis2g  22443  basdif0  22448  tgval2  22451  ntreq0  22573  isclo2  22584  opnnei  22616  neiptopnei  22628  lmres  22796  ist1-3  22845  cmpcov2  22886  cmpsub  22896  is1stc2  22938  1stccn  22959  kgencn  23052  eltx  23064  txkgen  23148  fbun  23336  trfbas  23340  fbunfip  23365  trfil2  23383  isufil2  23404  fixufil  23418  hausflim  23477  txflf  23502  fclsopn  23510  alexsubALTlem3  23545  isclmp  24605  iscau3  24787  iscau4  24788  caucfil  24792  bcth3  24840  ovolgelb  24989  dyadmax  25107  itg2leub  25244  itg2cn  25273  plydivex  25802  vieta1  25817  lgseisenlem2  26869  pnt3  27105  nosepon  27158  nomaxmo  27191  nosupbnd1lem4  27204  conway  27290  eqscut2  27297  etasslt  27304  slerec  27310  bday1s  27322  cuteq1  27324  madebdaylemlrcut  27383  addsproplem4  27446  addsproplem6  27448  addsprop  27450  addsuniflem  27474  mulsuniflem  27594  tglowdim2ln  27892  axcontlem12  28223  elntg2  28233  numedglnl  28394  vtxd0nedgb  28735  wlkvtxedg  28891  pthd  29016  2pthdlem1  29174  clwlkclwwlk  29245  3pthdlem1  29407  frgrregord013  29638  grpoidinvlem3  29747  nmoubi  30013  lnon0  30039  adjsym  31074  nmopub  31149  nmfnleub  31166  cvbr2  31524  chpssati  31604  chrelat2i  31606  chrelat3  31612  mdsymlem8  31651  ralcom4f  31697  reuxfrdf  31719  uniinn0  31770  ssiun3  31778  disjnf  31789  disjorf  31798  disjunsn  31813  ac6sf2  31837  nn0min  32014  tosglblem  32132  archiabl  32332  eulerpartlems  33348  eulerpartlemr  33362  eulerpartlemn  33369  ballotlem7  33523  bnj110  33858  bnj92  33862  bnj539  33891  bnj540  33892  bnj580  33913  bnj978  33949  bnj1047  33973  bnj1128  33990  bnj1417  34041  bnj1421  34042  bnj1312  34058  bnj1498  34061  lfuhgr3  34099  subfacp1lem3  34162  cvmlift2lem1  34282  cvmlift2lem12  34294  satfv1  34343  fmlaomn0  34370  fmla0disjsuc  34378  fmlasucdisj  34379  untuni  34667  dfso3  34678  elintfv  34725  setinds  34739  setinds2f  34740  elpotr  34742  dfon2lem7  34750  dfon2lem9  34752  dfint3  34913  brlb  34916  filnetlem4  35255  bj-reabeq  35897  ctbssinf  36276  fvineqsneq  36282  pibt2  36287  phpreu  36461  ptrecube  36477  poimirlem1  36478  poimirlem25  36502  poimirlem26  36503  poimirlem27  36504  poimirlem30  36507  mblfinlem2  36515  ftc1anc  36558  inixp  36585  ac6gf  36589  heibor1lem  36666  heiborlem1  36668  iscrngo2  36854  ac6s3f  37028  ref5  37171  idinxpssinxp2  37176  n0elqs  37184  ineleq  37212  refrelcosslem  37321  refrelcoss3  37322  lpssat  37872  lssat  37875  lcvbr2  37881  lcvbr3  37882  lfl1  37929  lub0N  38048  glb0N  38052  atlrelat1  38180  hlrelat2  38263  ispsubsp2  38606  pclclN  38751  cdleme25cv  39218  tendoeq2  39634  cdlemk35  39772  aks4d1p7  40937  sticksstones1  40951  infdesc  41382  setindtrs  41750  unielss  41953  ssunib  41955  onsupmaxb  41974  onsupeqnmax  41982  cllem0  42303  ntrneixb  42832  gneispace  42871  expandral  43035  ismnuprim  43039  dfuniv2  43047  undisjrab  43051  zfregs2VD  43588  iindif2f  43840  ralfal  43841  disjinfi  43877  iuneqfzuz  44032  caucvgbf  44187  rexanuz2nf  44190  mccl  44301  limsupub  44407  limsuppnflem  44413  limsupre2lem  44427  lmbr3v  44448  liminfpnfuz  44519  xlimpnfxnegmnf2  44561  ioodvbdlimc1lem2  44635  ioodvbdlimc2lem  44637  dvnprodlem3  44651  fourierdlem103  44912  fourierdlem104  44913  sge0iunmpt  45121  meaiuninc3v  45187  hoidmvle  45303  issmff  45437  n0nsn2el  45722  r19.32  45793  2rexrsb  45797  cbvral2  45798  2reu3  45805  2reu8i  45808  otiunsndisjX  45974  0nelsetpreimafv  46045  copisnmnd  46566  lindslinindsimp1  47092  lindslinindsimp2  47098  snlindsntor  47106  ldepslinc  47144  iscnrm3  47539  setrec1lem3  47688  aacllem  47802