Theorem ralbii 2980

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	|- ( ph <-> ps )

Assertion

Ref	Expression
ralbii	|- ( A. x e. A ph <-> A. x e. A ps )

Proof of Theorem ralbii

Step	Hyp	Ref	Expression
1		ralbii.1	. . 3 |- ( ph <-> ps )
2	1	imbi2i 326	. 2 |- ( ( x e. A -> ph ) <-> ( x e. A -> ps ) )
3	2	ralbii2 2978	1 |- ( A. x e. A ph <-> A. x e. A ps )

Syntax hints:   <-> wb 196   e. wcel 1990   A.wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  2ralbii  2981  dfral2  2994  ralinexa  2997  rexanali  2998  nrexralim  2999  r19.23v  3023  r19.26-2  3065  r19.26-3  3066  ralbiim  3069  r19.28v  3071  r19.30  3082  r19.32v  3083  r19.35  3084  ralcom13  3100  ralrot3  3102  cbvral2v  3179  cbvral3v  3181  sbralie  3184  ralcom4  3224  ralxpxfr2d  3327  reu8  3402  2reuswap  3410  2reu5lem2  3414  dfss5  3864  n0el  3940  ralnralall  4080  r19.12sn  4255  ssdifsn  4318  raldifsnb  4325  eqsn  4361  eqsnOLD  4362  n0snor2el  4364  uni0b  4463  uni0c  4464  ssint  4493  iuniin  4531  iuneq2  4537  iunss  4561  ssiinf  4569  iinab  4581  iinun2  4586  iindif2  4589  iinin2  4590  iinuni  4609  sspwuni  4611  iinpw  4617  disjor  4634  disjxun  4651  dftr3  4756  trint  4768  reusv3  4876  reuxfr2d  4891  otiunsndisj  4980  ssrel2  5210  reliun  5239  xpiindi  5257  rexiunxp  5262  ralxpf  5268  rexxpf  5269  dfse2  5499  asymref2  5513  rninxp  5573  dminxp  5574  cnviin  5672  cnvpo  5673  wfis2fg  5717  dffun9  5917  funcnv3  5959  fncnv  5962  fnres  6007  mptfnf  6015  fnopabg  6017  mptfng  6019  fint  6084  funimass4  6247  fndmdifeq0  6323  funconstss  6335  f1ompt  6382  fconstfv  6476  idref  6499  dff13f  6513  dff14b  6528  weniso  6604  foov  6808  dfwe2  6981  tfis2f  7055  tfindes  7062  frxp  7287  tz7.48lem  7536  tz7.49  7540  oeordi  7667  ixpeq2  7922  ixpin  7933  ixpiin  7934  boxriin  7950  findcard3  8203  fimax2g  8206  fissuni  8271  indexfi  8274  dfsup2  8350  sup0riota  8371  infcllem  8393  wemapsolem  8455  zfinf2  8539  oemapso  8579  zfregs2  8609  r1elss  8669  rankc1  8733  cp  8754  bnd2  8756  aceq1  8940  aceq2  8942  kmlem7  8978  kmlem12  8983  kmlem13  8984  kmlem15  8986  fin12  9235  ac6num  9301  ac6s2  9308  ac6sf  9311  ac6s4  9312  zorn2lem4  9321  zorn2lem6  9323  zorn2lem7  9324  zorng  9326  ttukeylem6  9336  brdom7disj  9353  brdom6disj  9354  fpwwe2  9465  fpwwe  9468  axgroth5  9646  axgroth4  9654  grothprim  9656  nqereu  9751  genpnnp  9827  dfinfre  11004  infrenegsup  11006  xrsupsslem  12137  xrinfmsslem  12138  xrinfmss2  12141  fzshftral  12428  fsuppmapnn0ub  12795  mptnn0fsuppr  12799  hashgt12el  13210  hashgt12el2  13211  hashbc  13237  s3iunsndisj  13707  cotr2g  13715  rexfiuz  14087  clim0  14237  rpnnen2lem12  14954  gcdcllem1  15221  absproddvds  15330  coprmproddvdslem  15376  vdwmc2  15683  vdwlem13  15697  vdwnn  15702  xpscf  16226  mreacs  16319  acsfn  16320  acsfn1  16322  acsfn2  16324  ispos2  16948  lublecllem  16988  oduglb  17139  odulub  17141  posglbd  17150  isnmnd  17298  gsumwspan  17383  isnsg2  17624  oppgid  17786  oppgcntz  17794  efgval2  18137  iscyggen2  18283  iscyg3  18288  oppr1  18634  isnirred  18700  lssne0  18951  isdomn2  19299  iunocv  20025  islindf4  20177  pmatcollpw2lem  20582  isbasis2g  20752  basdif0  20757  tgval2  20760  ntreq0  20881  isclo2  20892  opnnei  20924  neiptopnei  20936  lmres  21104  ist1-3  21153  cmpcov2  21193  cmpsub  21203  is1stc2  21245  1stccn  21266  kgencn  21359  eltx  21371  txkgen  21455  fbun  21644  trfbas  21648  fbunfip  21673  trfil2  21691  isufil2  21712  fixufil  21726  hausflim  21785  txflf  21810  fclsopn  21818  alexsubALTlem3  21853  isclmp  22897  iscau3  23076  iscau4  23077  caucfil  23081  bcth3  23128  ovolgelb  23248  dyadmax  23366  itg2leub  23501  itg2cn  23530  plydivex  24052  vieta1  24067  lgseisenlem2  25101  pnt3  25301  tglowdim2ln  25546  axcontlem12  25855  numedglnl  26039  vtxd0nedgb  26384  wlkvtxedg  26540  pthd  26665  2pthdlem1  26826  clwlkclwwlk  26903  clwlksfclwwlk  26962  3pthdlem1  27024  frgrregord013  27253  grpoidinvlem3  27360  nmoubi  27627  lnon0  27653  adjsym  28692  nmopub  28767  nmfnleub  28784  cvbr2  29142  chpssati  29222  chrelat2i  29224  chrelat3  29230  mdsymlem8  29269  ralcom4f  29316  moel  29323  uniinn0  29366  ssiun3  29376  disjnf  29384  disjorf  29392  disjunsn  29407  ac6sf2  29429  nn0min  29567  tosglblem  29669  archiabl  29752  eulerpartlems  30422  eulerpartlemr  30436  eulerpartlemn  30443  ballotlem7  30597  bnj110  30928  bnj92  30932  bnj539  30961  bnj540  30962  bnj580  30983  bnj978  31019  bnj1047  31041  bnj1128  31058  bnj1417  31109  bnj1421  31110  bnj1312  31126  bnj1498  31129  subfacp1lem3  31164  cvmlift2lem1  31284  cvmlift2lem12  31296  untuni  31586  dfso3  31601  dfpo2  31645  elintfv  31662  setinds  31683  setinds2f  31684  elpotr  31686  dfon2lem7  31694  dfon2lem9  31696  frins2fg  31744  soseq  31751  nosepon  31818  nomaxmo  31847  nosupbnd1lem4  31857  conway  31910  ssltun2  31916  etasslt  31920  slerec  31923  dfint3  32059  brlb  32062  gtinfOLD  32314  filnetlem4  32376  phpreu  33393  ptrecube  33409  poimirlem1  33410  poimirlem25  33434  poimirlem26  33435  poimirlem27  33436  poimirlem30  33439  mblfinlem2  33447  ftc1anc  33493  inixp  33523  ac6gf  33527  heibor1lem  33608  heiborlem1  33610  iscrngo2  33796  ac6s3f  33979  3ralbii  34013  idinxpssinxp2  34089  n0elqs  34098  ineleq  34119  lpssat  34300  lssat  34303  lcvbr2  34309  lcvbr3  34310  lfl1  34357  lub0N  34476  glb0N  34480  atlrelat1  34608  hlrelat2  34689  ispsubsp2  35032  pclclN  35177  cdleme25cv  35646  tendoeq2  36062  cdlemk35  36200  setindtrs  37592  cllem0  37871  ss2iundf  37951  ntrneixb  38393  gneispace  38432  undisjrab  38505  zfregs2VD  39076  iunssf  39263  disjinfi  39380  iuneqfzuz  39551  mccl  39830  limsupub  39936  limsuppnflem  39942  limsupre2lem  39956  lmbr3v  39977  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem3  40163  fourierdlem103  40426  fourierdlem104  40427  sge0iunmpt  40635  hoidmvle  40814  issmff  40943  r19.32  41167  2rexrsb  41171  cbvral2  41172  2ralbiim  41174  rmoanim  41179  2rmoswap  41184  2reu3  41188  2reu4a  41189  otiunsndisjX  41298  copisnmnd  41809  lindslinindsimp1  42246  lindslinindsimp2  42252  snlindsntor  42260  ldepslinc  42298  setrec1lem3  42436  aacllem  42547