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  3635  reu8  3730  2reuswap  3743  2reu5lem2  3753  2rmoswap  3758  rmoanim  3889  rmoanimALT  3890  dfss5  4265  n0el  4362  ralnralall  4519  2reu4lem  4526  r19.12sn  4725  raldifsnb  4800  eqsn  4833  n0snor2el  4835  uni0b  4938  uni0c  4939  ssint  4969  iuniin  5010  iuneq2  5017  iunssf  5048  iunss  5049  ssiinf  5058  iinab  5072  iinun2  5077  iindif1  5079  iindif2  5081  iinin2  5082  iinuni  5102  sspwuni  5104  iinpw  5110  disjor  5129  disjxun  5147  dftr3  5272  reusv3  5404  otiunsndisj  5521  ssrel2  5786  reliun  5817  xpiindi  5836  rexiunxp  5841  ralxpf  5847  rexxpf  5848  dfse2  6100  idrefALT  6113  asymref2  6119  rninxp  6179  dminxp  6180  cnviin  6286  cnvpo  6287  dfpo2  6296  dfse3  6338  frpoins2fg  6346  wfis2fgOLD  6359  dffun9  6578  funcnv3  6619  fncnv  6622  fnres  6678  mptfnf  6686  fnopabg  6688  mptfng  6690  fint  6771  funimass4  6957  fndmdifeq0  7046  funconstss  7058  f1ompt  7111  idref  7144  fconstfv  7214  dff13f  7255  dff14b  7270  weniso  7351  fnssintima  7359  foov  7581  imaeqalov  7646  dfwe2  7761  tfis2f  7845  tfindes  7852  frxp  8112  ralxp3f  8123  frpoins3xpg  8126  frpoins3xp3g  8127  xpord2indlem  8133  xpord3inddlem  8140  soseq  8145  dfwrecsOLD  8298  tz7.48lem  8441  tz7.49  8445  oeordi  8587  naddcllem  8675  naddunif  8692  naddasslem2  8694  ixpeq2  8905  ixpin  8917  ixpiin  8918  boxriin  8934  findcard3  9285  findcard3OLD  9286  fimax2g  9289  fissuni  9357  indexfi  9360  dfsup2  9439  sup0riota  9460  infcllem  9482  wemapsolem  9545  zfinf2  9637  oemapso  9677  ttrclresv  9712  zfregs2  9728  frins2f  9748  r1elss  9801  rankc1  9865  cp  9886  bnd2  9888  aceq1  10112  aceq2  10114  kmlem7  10151  kmlem12  10156  kmlem13  10157  kmlem15  10159  fin12  10408  ac6num  10474  ac6s2  10481  ac6sf  10484  ac6s4  10485  zorn2lem4  10494  zorn2lem6  10496  zorn2lem7  10497  zorng  10499  ttukeylem6  10509  brdom7disj  10526  brdom6disj  10527  fpwwe2  10638  fpwwe  10641  axgroth5  10819  axgroth4  10827  grothprim  10829  nqereu  10924  dfinfre  12195  infrenegsup  12197  xrsupsslem  13286  xrinfmsslem  13287  xrinfmss2  13290  fzshftral  13589  fsuppmapnn0ub  13960  mptnn0fsuppr  13964  hashgt12el  14382  hashgt12el2  14383  hashbc  14412  s3iunsndisj  14915  cotr2g  14923  rexfiuz  15294  clim0  15450  rpnnen2lem12  16168  gcdcllem1  16440  absproddvds  16554  coprmproddvdslem  16599  vdwmc2  16912  vdwlem13  16926  vdwnn  16931  xpscf  17511  mreacs  17602  acsfn  17603  acsfn1  17605  acsfn2  17607  dfinito2  17953  dftermo2  17954  ispos2  18268  lublecllem  18313  odulub  18360  oduglb  18362  posglbdg  18368  isnmnd  18629  gsumwspan  18727  smndex2dnrinv  18796  isnsg2  19036  oppgid  19223  oppgcntz  19231  efgval2  19592  iscyggen2  19749  iscyg3  19754  oppr1  20164  isnirred  20234  lssne0  20561  isdomn2  20915  isdomn5  20917  iunocv  21234  islindf4  21393  pmatcollpw2lem  22279  isbasis2g  22451  basdif0  22456  tgval2  22459  ntreq0  22581  isclo2  22592  opnnei  22624  neiptopnei  22636  lmres  22804  ist1-3  22853  cmpcov2  22894  cmpsub  22904  is1stc2  22946  1stccn  22967  kgencn  23060  eltx  23072  txkgen  23156  fbun  23344  trfbas  23348  fbunfip  23373  trfil2  23391  isufil2  23412  fixufil  23426  hausflim  23485  txflf  23510  fclsopn  23518  alexsubALTlem3  23553  isclmp  24613  iscau3  24795  iscau4  24796  caucfil  24800  bcth3  24848  ovolgelb  24997  dyadmax  25115  itg2leub  25252  itg2cn  25281  plydivex  25810  vieta1  25825  lgseisenlem2  26879  pnt3  27115  nosepon  27168  nomaxmo  27201  nosupbnd1lem4  27214  conway  27301  eqscut2  27308  etasslt  27315  slerec  27321  bday1s  27333  cuteq1  27335  madebdaylemlrcut  27394  addsproplem4  27458  addsproplem6  27460  addsprop  27462  addsuniflem  27487  mulsuniflem  27607  tglowdim2ln  27933  axcontlem12  28264  elntg2  28274  numedglnl  28435  vtxd0nedgb  28776  wlkvtxedg  28932  pthd  29057  2pthdlem1  29215  clwlkclwwlk  29286  3pthdlem1  29448  frgrregord013  29679  grpoidinvlem3  29790  nmoubi  30056  lnon0  30082  adjsym  31117  nmopub  31192  nmfnleub  31209  cvbr2  31567  chpssati  31647  chrelat2i  31649  chrelat3  31655  mdsymlem8  31694  ralcom4f  31740  reuxfrdf  31762  uniinn0  31813  ssiun3  31821  disjnf  31832  disjorf  31841  disjunsn  31856  ac6sf2  31880  nn0min  32057  tosglblem  32175  archiabl  32375  eulerpartlems  33390  eulerpartlemr  33404  eulerpartlemn  33411  ballotlem7  33565  bnj110  33900  bnj92  33904  bnj539  33933  bnj540  33934  bnj580  33955  bnj978  33991  bnj1047  34015  bnj1128  34032  bnj1417  34083  bnj1421  34084  bnj1312  34100  bnj1498  34103  lfuhgr3  34141  subfacp1lem3  34204  cvmlift2lem1  34324  cvmlift2lem12  34336  satfv1  34385  fmlaomn0  34412  fmla0disjsuc  34420  fmlasucdisj  34421  untuni  34709  dfso3  34720  elintfv  34767  setinds  34781  setinds2f  34782  elpotr  34784  dfon2lem7  34792  dfon2lem9  34794  dfint3  34955  brlb  34958  filnetlem4  35314  bj-reabeq  35956  ctbssinf  36335  fvineqsneq  36341  pibt2  36346  phpreu  36520  ptrecube  36536  poimirlem1  36537  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem30  36566  mblfinlem2  36574  ftc1anc  36617  inixp  36644  ac6gf  36648  heibor1lem  36725  heiborlem1  36727  iscrngo2  36913  ac6s3f  37087  ref5  37230  idinxpssinxp2  37235  n0elqs  37243  ineleq  37271  refrelcosslem  37380  refrelcoss3  37381  lpssat  37931  lssat  37934  lcvbr2  37940  lcvbr3  37941  lfl1  37988  lub0N  38107  glb0N  38111  atlrelat1  38239  hlrelat2  38322  ispsubsp2  38665  pclclN  38810  cdleme25cv  39277  tendoeq2  39693  cdlemk35  39831  aks4d1p7  40996  sticksstones1  41010  infdesc  41433  setindtrs  41812  unielss  42015  ssunib  42017  onsupmaxb  42036  onsupeqnmax  42044  cllem0  42365  ntrneixb  42894  gneispace  42933  expandral  43097  ismnuprim  43101  dfuniv2  43109  undisjrab  43113  zfregs2VD  43650  iindif2f  43902  ralfal  43903  disjinfi  43939  iuneqfzuz  44093  caucvgbf  44248  rexanuz2nf  44251  mccl  44362  limsupub  44468  limsuppnflem  44474  limsupre2lem  44488  lmbr3v  44509  liminfpnfuz  44580  xlimpnfxnegmnf2  44622  ioodvbdlimc1lem2  44696  ioodvbdlimc2lem  44698  dvnprodlem3  44712  fourierdlem103  44973  fourierdlem104  44974  sge0iunmpt  45182  meaiuninc3v  45248  hoidmvle  45364  issmff  45498  n0nsn2el  45783  r19.32  45854  2rexrsb  45858  cbvral2  45859  2reu3  45866  2reu8i  45869  otiunsndisjX  46035  0nelsetpreimafv  46106  copisnmnd  46627  lindslinindsimp1  47186  lindslinindsimp2  47192  snlindsntor  47200  ldepslinc  47238  iscnrm3  47633  setrec1lem3  47782  aacllem  47896