Theorem ralbii 3165

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

Syntax hints:   ↔ wb 208   ∈ wcel 2114  ∀wral 3138

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

This theorem depends on definitions:  df-bi 209  df-ral 3143

This theorem is referenced by:  2ralbii  3166  r19.26-2  3171  r19.26-3  3172  ralbiim  3174  r19.28vOLD  3187  dfral2  3237  ralnex2  3260  ralinexa  3264  rexanali  3265  nrexralim  3266  nelb  3268  r19.23v  3279  r19.30OLD  3339  r19.32v  3340  ralcom13  3359  ralrot3  3361  cbvral2vw  3461  cbvral3vw  3463  cbvral2v  3464  cbvral3v  3466  sbralie  3471  ralcom4OLD  3525  ralxpxfr2d  3639  reu8  3724  2reuswap  3737  2reu5lem2  3747  2rmoswap  3752  rmoanim  3878  rmoanimALT  3879  dfss5  4241  n0el  4321  ralnralall  4458  2reu4lem  4465  r19.12sn  4656  raldifsnb  4729  eqsn  4762  n0snor2el  4764  uni0b  4864  uni0c  4865  ssint  4892  iuniin  4931  iuneq2  4938  iunss  4969  ssiinf  4978  iinab  4990  iinun2  4995  iindif1  4997  iindif2  4999  iinin2  5000  iinuni  5020  sspwuni  5022  iinpw  5028  disjor  5046  disjxun  5064  dftr3  5176  reusv3  5306  otiunsndisj  5410  ssrel2  5659  reliun  5689  xpiindi  5706  rexiunxp  5711  ralxpf  5717  rexxpf  5718  dfse2  5963  idrefALT  5973  asymref2  5977  rninxp  6036  dminxp  6037  cnviin  6137  cnvpo  6138  wfis2fg  6185  dffun9  6384  funcnv3  6424  fncnv  6427  fnres  6474  mptfnf  6483  fnopabg  6485  mptfng  6487  fint  6558  funimass4  6730  fndmdifeq0  6814  funconstss  6826  f1ompt  6875  idref  6908  fconstfv  6975  dff13f  7014  dff14b  7029  weniso  7107  foov  7322  dfwe2  7496  tfis2f  7570  tfindes  7577  frxp  7820  tz7.48lem  8077  tz7.49  8081  oeordi  8213  ixpeq2  8475  ixpin  8487  ixpiin  8488  boxriin  8504  findcard3  8761  fimax2g  8764  fissuni  8829  indexfi  8832  dfsup2  8908  sup0riota  8929  infcllem  8951  wemapsolem  9014  zfinf2  9105  oemapso  9145  zfregs2  9175  r1elss  9235  rankc1  9299  cp  9320  bnd2  9322  aceq1  9543  aceq2  9545  kmlem7  9582  kmlem12  9587  kmlem13  9588  kmlem15  9590  fin12  9835  ac6num  9901  ac6s2  9908  ac6sf  9911  ac6s4  9912  zorn2lem4  9921  zorn2lem6  9923  zorn2lem7  9924  zorng  9926  ttukeylem6  9936  brdom7disj  9953  brdom6disj  9954  fpwwe2  10065  fpwwe  10068  axgroth5  10246  axgroth4  10254  grothprim  10256  nqereu  10351  dfinfre  11622  infrenegsup  11624  xrsupsslem  12701  xrinfmsslem  12702  xrinfmss2  12705  fzshftral  12996  fsuppmapnn0ub  13364  mptnn0fsuppr  13368  hashgt12el  13784  hashgt12el2  13785  hashbc  13812  s3iunsndisj  14328  cotr2g  14336  rexfiuz  14707  clim0  14863  rpnnen2lem12  15578  gcdcllem1  15848  absproddvds  15961  coprmproddvdslem  16006  vdwmc2  16315  vdwlem13  16329  vdwnn  16334  xpscf  16838  mreacs  16929  acsfn  16930  acsfn1  16932  acsfn2  16934  ispos2  17558  lublecllem  17598  oduglb  17749  odulub  17751  posglbd  17760  isnmnd  17915  gsumwspan  18011  smndex2dnrinv  18080  isnsg2  18308  oppgid  18484  oppgcntz  18492  efgval2  18850  iscyggen2  19000  iscyg3  19005  oppr1  19384  isnirred  19450  lssne0  19722  isdomn2  20072  iunocv  20825  islindf4  20982  pmatcollpw2lem  21385  isbasis2g  21556  basdif0  21561  tgval2  21564  ntreq0  21685  isclo2  21696  opnnei  21728  neiptopnei  21740  lmres  21908  ist1-3  21957  cmpcov2  21998  cmpsub  22008  is1stc2  22050  1stccn  22071  kgencn  22164  eltx  22176  txkgen  22260  fbun  22448  trfbas  22452  fbunfip  22477  trfil2  22495  isufil2  22516  fixufil  22530  hausflim  22589  txflf  22614  fclsopn  22622  alexsubALTlem3  22657  isclmp  23701  iscau3  23881  iscau4  23882  caucfil  23886  bcth3  23934  ovolgelb  24081  dyadmax  24199  itg2leub  24335  itg2cn  24364  plydivex  24886  vieta1  24901  lgseisenlem2  25952  pnt3  26188  tglowdim2ln  26437  axcontlem12  26761  elntg2  26771  numedglnl  26929  vtxd0nedgb  27270  wlkvtxedg  27425  pthd  27550  2pthdlem1  27709  clwlkclwwlk  27780  3pthdlem1  27943  frgrregord013  28174  grpoidinvlem3  28283  nmoubi  28549  lnon0  28575  adjsym  29610  nmopub  29685  nmfnleub  29702  cvbr2  30060  chpssati  30140  chrelat2i  30142  chrelat3  30148  mdsymlem8  30187  nelbOLD  30232  ralcom4f  30233  moel  30252  reuxfrdf  30255  uniinn0  30302  ssiun3  30310  disjnf  30320  disjorf  30329  disjunsn  30344  ac6sf2  30370  nn0min  30536  tosglblem  30656  archiabl  30827  eulerpartlems  31618  eulerpartlemr  31632  eulerpartlemn  31639  ballotlem7  31793  bnj110  32130  bnj92  32134  bnj539  32163  bnj540  32164  bnj580  32185  bnj978  32221  bnj1047  32245  bnj1128  32262  bnj1417  32313  bnj1421  32314  bnj1312  32330  bnj1498  32333  lfuhgr3  32366  subfacp1lem3  32429  cvmlift2lem1  32549  cvmlift2lem12  32561  satfv1  32610  fmlaomn0  32637  fmla0disjsuc  32645  fmlasucdisj  32646  untuni  32935  dfso3  32950  dfpo2  32991  elintfv  33007  setinds  33023  setinds2f  33024  elpotr  33026  dfon2lem7  33034  dfon2lem9  33036  frpoins2fg  33082  frins2fg  33089  soseq  33096  nosepon  33172  nomaxmo  33201  nosupbnd1lem4  33211  conway  33264  ssltun2  33270  etasslt  33274  slerec  33277  dfint3  33413  brlb  33416  filnetlem4  33729  bj-reabeq  34342  ctbssinf  34690  fvineqsneq  34696  pibt2  34701  phpreu  34891  ptrecube  34907  poimirlem1  34908  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem30  34937  mblfinlem2  34945  ftc1anc  34990  inixp  35018  ac6gf  35022  heibor1lem  35102  heiborlem1  35104  iscrngo2  35290  ac6s3f  35464  3ralbii  35525  idinxpssinxp2  35590  n0elqs  35598  ineleq  35623  refrelcosslem  35717  refrelcoss3  35718  lpssat  36164  lssat  36167  lcvbr2  36173  lcvbr3  36174  lfl1  36221  lub0N  36340  glb0N  36344  atlrelat1  36472  hlrelat2  36554  ispsubsp2  36897  pclclN  37042  cdleme25cv  37509  tendoeq2  37925  cdlemk35  38063  setindtrs  39642  cllem0  39945  ss2iundf  40024  ntrneixb  40465  gneispace  40504  expandral  40646  ismnuprim  40650  undisjrab  40658  zfregs2VD  41195  iunssf  41372  disjinfi  41474  iuneqfzuz  41623  mccl  41899  limsupub  42005  limsuppnflem  42011  limsupre2lem  42025  lmbr3v  42046  liminfpnfuz  42117  xlimpnfxnegmnf2  42159  ioodvbdlimc1lem2  42237  ioodvbdlimc2lem  42239  dvnprodlem3  42253  fourierdlem103  42514  fourierdlem104  42515  sge0iunmpt  42720  meaiuninc3v  42786  hoidmvle  42902  issmff  43031  r19.32  43316  2rexrsb  43320  cbvral2  43321  2ralbiim  43323  2reu3  43329  2reu8i  43332  otiunsndisjX  43498  0nelsetpreimafv  43570  copisnmnd  44096  lindslinindsimp1  44532  lindslinindsimp2  44538  snlindsntor  44546  ldepslinc  44584  setrec1lem3  44812  aacllem  44922