Theorem ralbii 3167

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 3165	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

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

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 3145

This theorem is referenced by:  2ralbii  3168  r19.26-2  3173  r19.26-3  3174  ralbiim  3176  r19.28vOLD  3189  dfral2  3239  ralnex2  3262  ralinexa  3266  rexanali  3267  nrexralim  3268  nelb  3270  r19.23v  3281  r19.30OLD  3341  r19.32v  3342  ralcom13  3361  ralrot3  3363  cbvral2vw  3463  cbvral3vw  3465  cbvral2v  3466  cbvral3v  3468  sbralie  3473  ralcom4OLD  3527  ralxpxfr2d  3641  reu8  3726  2reuswap  3739  2reu5lem2  3749  2rmoswap  3754  rmoanim  3880  rmoanimALT  3881  dfss5  4243  n0el  4323  ralnralall  4460  2reu4lem  4467  r19.12sn  4658  raldifsnb  4731  eqsn  4764  n0snor2el  4766  uni0b  4866  uni0c  4867  ssint  4894  iuniin  4933  iuneq2  4940  iunss  4971  ssiinf  4980  iinab  4992  iinun2  4997  iindif1  4999  iindif2  5001  iinin2  5002  iinuni  5022  sspwuni  5024  iinpw  5030  disjor  5048  disjxun  5066  dftr3  5178  reusv3  5308  otiunsndisj  5412  ssrel2  5661  reliun  5691  xpiindi  5708  rexiunxp  5713  ralxpf  5719  rexxpf  5720  dfse2  5965  idrefALT  5975  asymref2  5979  rninxp  6038  dminxp  6039  cnviin  6139  cnvpo  6140  wfis2fg  6187  dffun9  6386  funcnv3  6426  fncnv  6429  fnres  6476  mptfnf  6485  fnopabg  6487  mptfng  6489  fint  6560  funimass4  6732  fndmdifeq0  6816  funconstss  6828  f1ompt  6877  idref  6910  fconstfv  6977  dff13f  7016  dff14b  7031  weniso  7109  foov  7324  dfwe2  7498  tfis2f  7572  tfindes  7579  frxp  7822  tz7.48lem  8079  tz7.49  8083  oeordi  8215  ixpeq2  8477  ixpin  8489  ixpiin  8490  boxriin  8506  findcard3  8763  fimax2g  8766  fissuni  8831  indexfi  8834  dfsup2  8910  sup0riota  8931  infcllem  8953  wemapsolem  9016  zfinf2  9107  oemapso  9147  zfregs2  9177  r1elss  9237  rankc1  9301  cp  9322  bnd2  9324  aceq1  9545  aceq2  9547  kmlem7  9584  kmlem12  9589  kmlem13  9590  kmlem15  9592  fin12  9837  ac6num  9903  ac6s2  9910  ac6sf  9913  ac6s4  9914  zorn2lem4  9923  zorn2lem6  9925  zorn2lem7  9926  zorng  9928  ttukeylem6  9938  brdom7disj  9955  brdom6disj  9956  fpwwe2  10067  fpwwe  10070  axgroth5  10248  axgroth4  10256  grothprim  10258  nqereu  10353  dfinfre  11624  infrenegsup  11626  xrsupsslem  12703  xrinfmsslem  12704  xrinfmss2  12707  fzshftral  12998  fsuppmapnn0ub  13366  mptnn0fsuppr  13370  hashgt12el  13786  hashgt12el2  13787  hashbc  13814  s3iunsndisj  14330  cotr2g  14338  rexfiuz  14709  clim0  14865  rpnnen2lem12  15580  gcdcllem1  15850  absproddvds  15963  coprmproddvdslem  16008  vdwmc2  16317  vdwlem13  16331  vdwnn  16336  xpscf  16840  mreacs  16931  acsfn  16932  acsfn1  16934  acsfn2  16936  ispos2  17560  lublecllem  17600  oduglb  17751  odulub  17753  posglbd  17762  isnmnd  17917  gsumwspan  18013  smndex2dnrinv  18082  isnsg2  18310  oppgid  18486  oppgcntz  18494  efgval2  18852  iscyggen2  19002  iscyg3  19007  oppr1  19386  isnirred  19452  lssne0  19724  isdomn2  20074  iunocv  20827  islindf4  20984  pmatcollpw2lem  21387  isbasis2g  21558  basdif0  21563  tgval2  21566  ntreq0  21687  isclo2  21698  opnnei  21730  neiptopnei  21742  lmres  21910  ist1-3  21959  cmpcov2  22000  cmpsub  22010  is1stc2  22052  1stccn  22073  kgencn  22166  eltx  22178  txkgen  22262  fbun  22450  trfbas  22454  fbunfip  22479  trfil2  22497  isufil2  22518  fixufil  22532  hausflim  22591  txflf  22616  fclsopn  22624  alexsubALTlem3  22659  isclmp  23703  iscau3  23883  iscau4  23884  caucfil  23888  bcth3  23936  ovolgelb  24083  dyadmax  24201  itg2leub  24337  itg2cn  24366  plydivex  24888  vieta1  24903  lgseisenlem2  25954  pnt3  26190  tglowdim2ln  26439  axcontlem12  26763  elntg2  26773  numedglnl  26931  vtxd0nedgb  27272  wlkvtxedg  27427  pthd  27552  2pthdlem1  27711  clwlkclwwlk  27782  3pthdlem1  27945  frgrregord013  28176  grpoidinvlem3  28285  nmoubi  28551  lnon0  28577  adjsym  29612  nmopub  29687  nmfnleub  29704  cvbr2  30062  chpssati  30142  chrelat2i  30144  chrelat3  30150  mdsymlem8  30189  nelbOLD  30234  ralcom4f  30235  moel  30254  reuxfrdf  30257  uniinn0  30304  ssiun3  30312  disjnf  30322  disjorf  30331  disjunsn  30346  ac6sf2  30372  nn0min  30538  tosglblem  30658  archiabl  30829  eulerpartlems  31620  eulerpartlemr  31634  eulerpartlemn  31641  ballotlem7  31795  bnj110  32132  bnj92  32136  bnj539  32165  bnj540  32166  bnj580  32187  bnj978  32223  bnj1047  32247  bnj1128  32264  bnj1417  32315  bnj1421  32316  bnj1312  32332  bnj1498  32335  lfuhgr3  32368  subfacp1lem3  32431  cvmlift2lem1  32551  cvmlift2lem12  32563  satfv1  32612  fmlaomn0  32639  fmla0disjsuc  32647  fmlasucdisj  32648  untuni  32937  dfso3  32952  dfpo2  32993  elintfv  33009  setinds  33025  setinds2f  33026  elpotr  33028  dfon2lem7  33036  dfon2lem9  33038  frpoins2fg  33084  frins2fg  33091  soseq  33098  nosepon  33174  nomaxmo  33203  nosupbnd1lem4  33213  conway  33266  ssltun2  33272  etasslt  33276  slerec  33279  dfint3  33415  brlb  33418  filnetlem4  33731  bj-reabeq  34341  ctbssinf  34689  fvineqsneq  34695  pibt2  34700  phpreu  34878  ptrecube  34894  poimirlem1  34895  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem30  34924  mblfinlem2  34932  ftc1anc  34977  inixp  35005  ac6gf  35009  heibor1lem  35089  heiborlem1  35091  iscrngo2  35277  ac6s3f  35451  3ralbii  35512  idinxpssinxp2  35577  n0elqs  35585  ineleq  35610  refrelcosslem  35704  refrelcoss3  35705  lpssat  36151  lssat  36154  lcvbr2  36160  lcvbr3  36161  lfl1  36208  lub0N  36327  glb0N  36331  atlrelat1  36459  hlrelat2  36541  ispsubsp2  36884  pclclN  37029  cdleme25cv  37496  tendoeq2  37912  cdlemk35  38050  setindtrs  39629  cllem0  39932  ss2iundf  40011  ntrneixb  40452  gneispace  40491  expandral  40633  ismnuprim  40637  undisjrab  40645  zfregs2VD  41182  iunssf  41359  disjinfi  41461  iuneqfzuz  41610  mccl  41886  limsupub  41992  limsuppnflem  41998  limsupre2lem  42012  lmbr3v  42033  liminfpnfuz  42104  xlimpnfxnegmnf2  42146  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnprodlem3  42240  fourierdlem103  42501  fourierdlem104  42502  sge0iunmpt  42707  meaiuninc3v  42773  hoidmvle  42889  issmff  43018  r19.32  43303  2rexrsb  43307  cbvral2  43308  2ralbiim  43310  2reu3  43316  2reu8i  43319  otiunsndisjX  43485  0nelsetpreimafv  43557  copisnmnd  44083  lindslinindsimp1  44519  lindslinindsimp2  44525  snlindsntor  44533  ldepslinc  44571  setrec1lem3  44799  aacllem  44909