Theorem ralbii 3168

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	imbi2i 327	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3166	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   ↔ wb 197   ∈ wcel 2156  ∀wral 3096

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

This theorem depends on definitions:  df-bi 198  df-ral 3101

This theorem is referenced by:  2ralbii  3169  dfral2  3181  ralinexa  3184  rexanali  3185  nrexralim  3186  r19.23v  3211  r19.26-2  3253  r19.26-3  3254  ralbiim  3257  r19.28v  3259  r19.30  3270  r19.32v  3271  r19.35  3272  ralcom13  3288  ralrot3  3290  cbvral2v  3368  cbvral3v  3370  sbralie  3373  ralcom4  3418  ralxpxfr2d  3521  reu8  3600  2reuswap  3608  2reu5lem2  3612  dfss5  4066  n0el  4141  ralnralall  4273  r19.12sn  4446  ssdifsnOLD  4510  raldifsnb  4517  eqsn  4550  n0snor2el  4552  uni0b  4657  uni0c  4658  ssint  4685  iuniin  4723  iuneq2  4729  iunss  4753  ssiinf  4761  iinab  4773  iinun2  4778  iindif2  4781  iinin2  4782  iinuni  4801  sspwuni  4803  iinpw  4809  disjor  4826  disjxun  4842  dftr3  4950  trint  4961  reusv3  5074  reuxfr2d  5088  otiunsndisj  5175  ssrel2  5412  reliun  5441  xpiindi  5459  rexiunxp  5464  ralxpf  5470  rexxpf  5471  dfse2  5709  idrefALT  5719  asymref2  5724  rninxp  5784  dminxp  5785  cnviin  5886  cnvpo  5887  wfis2fg  5930  dffun9  6130  funcnv3  6170  fncnv  6173  fnres  6218  mptfnf  6226  fnopabg  6228  mptfng  6230  fint  6299  funimass4  6468  fndmdifeq0  6545  funconstss  6557  f1ompt  6603  idref  6635  fconstfv  6701  dff13f  6737  dff14b  6752  weniso  6828  foov  7038  dfwe2  7211  tfis2f  7285  tfindes  7292  frxp  7521  tz7.48lem  7772  tz7.49  7776  oeordi  7904  ixpeq2  8159  ixpin  8170  ixpiin  8171  boxriin  8187  findcard3  8442  fimax2g  8445  fissuni  8510  indexfi  8513  dfsup2  8589  sup0riota  8610  infcllem  8632  wemapsolem  8694  zfinf2  8786  oemapso  8826  zfregs2  8856  r1elss  8916  rankc1  8980  cp  9001  bnd2  9003  aceq1  9223  aceq2  9225  kmlem7  9263  kmlem12  9268  kmlem13  9269  kmlem15  9271  fin12  9520  ac6num  9586  ac6s2  9593  ac6sf  9596  ac6s4  9597  zorn2lem4  9606  zorn2lem6  9608  zorn2lem7  9609  zorng  9611  ttukeylem6  9621  brdom7disj  9638  brdom6disj  9639  fpwwe2  9750  fpwwe  9753  axgroth5  9931  axgroth4  9939  grothprim  9941  nqereu  10036  genpnnp  10112  dfinfre  11289  infrenegsup  11291  xrsupsslem  12355  xrinfmsslem  12356  xrinfmss2  12359  fzshftral  12651  fsuppmapnn0ub  13018  mptnn0fsuppr  13022  hashgt12el  13427  hashgt12el2  13428  hashbc  13454  s3iunsndisj  13932  cotr2g  13940  rexfiuz  14310  clim0  14460  rpnnen2lem12  15174  gcdcllem1  15440  absproddvds  15549  coprmproddvdslem  15594  vdwmc2  15900  vdwlem13  15914  vdwnn  15919  xpscf  16431  mreacs  16523  acsfn  16524  acsfn1  16526  acsfn2  16528  ispos2  17153  lublecllem  17193  oduglb  17344  odulub  17346  posglbd  17355  isnmnd  17503  gsumwspan  17588  isnsg2  17826  oppgid  17987  oppgcntz  17995  efgval2  18338  iscyggen2  18484  iscyg3  18489  oppr1  18836  isnirred  18902  lssne0  19155  isdomn2  19508  iunocv  20235  islindf4  20387  pmatcollpw2lem  20795  isbasis2g  20966  basdif0  20971  tgval2  20974  ntreq0  21095  isclo2  21106  opnnei  21138  neiptopnei  21150  lmres  21318  ist1-3  21367  cmpcov2  21407  cmpsub  21417  is1stc2  21459  1stccn  21480  kgencn  21573  eltx  21585  txkgen  21669  fbun  21857  trfbas  21861  fbunfip  21886  trfil2  21904  isufil2  21925  fixufil  21939  hausflim  21998  txflf  22023  fclsopn  22031  alexsubALTlem3  22066  isclmp  23109  iscau3  23288  iscau4  23289  caucfil  23293  bcth3  23340  ovolgelb  23461  dyadmax  23579  itg2leub  23715  itg2cn  23744  plydivex  24266  vieta1  24281  lgseisenlem2  25315  pnt3  25515  tglowdim2ln  25760  axcontlem12  26069  numedglnl  26254  vtxd0nedgb  26612  wlkvtxedg  26768  pthd  26893  2pthdlem1  27070  clwlkclwwlk  27145  clwlksfclwwlkOLD  27236  3pthdlem1  27337  frgrregord013  27583  grpoidinvlem3  27689  nmoubi  27955  lnon0  27981  adjsym  29020  nmopub  29095  nmfnleub  29112  cvbr2  29470  chpssati  29550  chrelat2i  29552  chrelat3  29558  mdsymlem8  29597  ralcom4f  29644  moel  29651  uniinn0  29691  ssiun3  29701  disjnf  29709  disjorf  29717  disjunsn  29732  ac6sf2  29756  nn0min  29894  tosglblem  29994  archiabl  30077  eulerpartlems  30747  eulerpartlemr  30761  eulerpartlemn  30768  ballotlem7  30922  bnj110  31251  bnj92  31255  bnj539  31284  bnj540  31285  bnj580  31306  bnj978  31342  bnj1047  31364  bnj1128  31381  bnj1417  31432  bnj1421  31433  bnj1312  31449  bnj1498  31452  subfacp1lem3  31487  cvmlift2lem1  31607  cvmlift2lem12  31619  untuni  31908  dfso3  31923  dfpo2  31967  elintfv  31984  setinds  32003  setinds2f  32004  elpotr  32006  dfon2lem7  32014  dfon2lem9  32016  frins2fg  32068  soseq  32075  nosepon  32139  nomaxmo  32168  nosupbnd1lem4  32178  conway  32231  ssltun2  32237  etasslt  32241  slerec  32244  dfint3  32380  brlb  32383  gtinfOLD  32635  filnetlem4  32697  phpreu  33706  ptrecube  33722  poimirlem1  33723  poimirlem25  33747  poimirlem26  33748  poimirlem27  33749  poimirlem30  33752  mblfinlem2  33760  ftc1anc  33805  inixp  33835  ac6gf  33839  heibor1lem  33919  heiborlem1  33921  iscrngo2  34107  ac6s3f  34289  3ralbii  34332  idinxpssinxp2  34404  n0elqs  34413  ineleq  34432  refrelcosslem  34525  refrelcoss3  34526  lpssat  34793  lssat  34796  lcvbr2  34802  lcvbr3  34803  lfl1  34850  lub0N  34969  glb0N  34973  atlrelat1  35101  hlrelat2  35183  ispsubsp2  35526  pclclN  35671  cdleme25cv  36139  tendoeq2  36555  cdlemk35  36693  setindtrs  38093  cllem0  38371  ss2iundf  38451  ntrneixb  38893  gneispace  38932  undisjrab  39005  zfregs2VD  39570  iunssf  39756  disjinfi  39869  iuneqfzuz  40031  mccl  40310  limsupub  40416  limsuppnflem  40422  limsupre2lem  40436  lmbr3v  40457  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnprodlem3  40643  fourierdlem103  40905  fourierdlem104  40906  sge0iunmpt  41114  meaiuninc3v  41180  hoidmvle  41296  issmff  41425  r19.32  41680  2rexrsb  41684  cbvral2  41685  2ralbiim  41687  rmoanim  41691  2rmoswap  41696  2reu3  41700  2reu4a  41701  otiunsndisjX  41869  copisnmnd  42377  lindslinindsimp1  42814  lindslinindsimp2  42820  snlindsntor  42828  ldepslinc  42866  setrec1lem3  43004  aacllem  43118