Theorem ralbii 3082

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

Syntax hints:   ↔ wb 206   ∈ wcel 2113  ∀wral 3051

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 207  df-ral 3052

This theorem is referenced by:  dfral2  3087  ralinexa  3089  rexanali  3090  r19.26-3  3097  ralbiim  3098  2ralbii  3111  3ralbii  3113  4ralbii  3114  2ralbiim  3115  ralnex2  3116  nrexralim  3120  r19.26-2  3121  r19.23v  3163  r19.32v  3169  2ralor  3210  nelb  3212  cbvral2vw  3218  cbvral3vw  3220  ralrot3  3267  ralcom13  3268  sbralieALT  3323  cbvral2v  3338  cbvral3v  3340  ceqsralv  3481  ralxpxfr2d  3600  reu8  3691  2reuswap  3704  2reu5lem2  3714  2rmoswap  3719  rmoanim  3844  rmoanimALT  3845  dfdif3  4069  dfss5  4227  n0el  4316  ralnralall  4466  2reu4lem  4476  r19.12sn  4677  raldifsnb  4752  eqsn  4785  n0snor2el  4789  uni0b  4889  uni0c  4890  ssint  4919  iuniin  4959  iuneq2  4966  iunssf  4998  iunssfOLD  4999  iunss  5000  iunssOLD  5001  ssiinf  5010  iinab  5023  iinun2  5028  iindif1  5030  iindif2  5032  iinin2  5033  iinuni  5053  sspwuni  5055  iinpw  5061  disjor  5080  disjxun  5096  dftr3  5210  reusv3  5350  otiunsndisj  5468  ssrel2  5734  reliun  5765  xpiindi  5784  rexiunxp  5789  ralxpf  5795  rexxpf  5796  dfse2  6059  idrefALT  6070  asymref2  6074  rninxp  6137  dminxp  6138  cnviin  6244  cnvpo  6245  dfpo2  6254  dfse3  6294  frpoins2fg  6302  dffun9  6521  funcnv3  6562  fncnv  6565  fnres  6619  mptfnf  6627  fnopabg  6629  mptfng  6631  fint  6713  funimass4  6898  fndmdifeq0  6989  funconstss  7001  f1ompt  7056  idref  7091  fconstfv  7158  dff13f  7201  dff14b  7217  weniso  7300  fnssintima  7308  foov  7532  imaeqalov  7597  dfwe2  7719  tfis2f  7798  tfindes  7805  frxp  8068  ralxp3f  8079  frpoins3xpg  8082  frpoins3xp3g  8083  xpord2indlem  8089  xpord3inddlem  8096  soseq  8101  tz7.48lem  8372  tz7.49  8376  oeordi  8515  naddcllem  8604  naddunif  8621  naddasslem2  8623  ixpeq2  8849  ixpin  8861  ixpiin  8862  boxriin  8878  findcard3  9183  fimax2g  9186  fissuni  9257  indexfi  9260  dfsup2  9347  sup0riota  9369  infcllem  9391  wemapsolem  9455  zfinf2  9551  oemapso  9591  ttrclresv  9626  zfregs2  9642  setinds  9658  setinds2f  9659  frins2f  9665  r1elss  9718  rankc1  9782  cp  9803  bnd2  9805  aceq1  10027  aceq2  10029  kmlem7  10067  kmlem12  10072  kmlem13  10073  kmlem15  10075  fin12  10323  ac6num  10389  ac6s2  10396  ac6sf  10399  ac6s4  10400  zorn2lem4  10409  zorn2lem6  10411  zorn2lem7  10412  zorng  10414  ttukeylem6  10424  brdom7disj  10441  brdom6disj  10442  fpwwe2  10554  fpwwe  10557  axgroth5  10735  axgroth4  10743  grothprim  10745  nqereu  10840  dfinfre  12123  infrenegsup  12125  xrsupsslem  13222  xrinfmsslem  13223  xrinfmss2  13226  fzshftral  13531  fsuppmapnn0ub  13918  mptnn0fsuppr  13922  hashgt12el  14345  hashgt12el2  14346  hashbc  14376  s3iunsndisj  14891  cotr2g  14899  rexfiuz  15271  clim0  15429  rpnnen2lem12  16150  gcdcllem1  16426  absproddvds  16544  coprmproddvdslem  16589  vdwmc2  16907  vdwlem13  16921  vdwnn  16926  xpscf  17486  mreacs  17581  acsfn  17582  acsfn1  17584  acsfn2  17586  dfinito2  17927  dftermo2  17928  ispos2  18238  lublecllem  18281  odulub  18328  oduglb  18330  posglbdg  18336  isnmnd  18663  gsumwspan  18771  smndex2dnrinv  18840  isnsg2  19085  oppgid  19285  oppgcntz  19293  efgval2  19653  iscyggen2  19810  iscyg3  19815  oppr1  20286  isnirred  20356  isdomn5  20643  isdomn2OLD  20645  lssne0  20902  iunocv  21636  islindf4  21793  pmatcollpw2lem  22721  isbasis2g  22892  basdif0  22897  tgval2  22900  ntreq0  23021  isclo2  23032  opnnei  23064  neiptopnei  23076  lmres  23244  ist1-3  23293  cmpcov2  23334  cmpsub  23344  is1stc2  23386  1stccn  23407  kgencn  23500  eltx  23512  txkgen  23596  fbun  23784  trfbas  23788  fbunfip  23813  trfil2  23831  isufil2  23852  fixufil  23866  hausflim  23925  txflf  23950  fclsopn  23958  alexsubALTlem3  23993  isclmp  25053  iscau3  25234  iscau4  25235  caucfil  25239  bcth3  25287  ovolgelb  25437  dyadmax  25555  itg2leub  25691  itg2cn  25720  plydivex  26261  vieta1  26276  lgseisenlem2  27343  pnt3  27579  nosepon  27633  nomaxmo  27666  nosupbnd1lem4  27679  conway  27775  eqcuts2  27782  etaslts  27789  lesrec  27795  bday1  27810  cuteq1  27813  madebdaylemlrcut  27895  addsproplem4  27968  addsproplem6  27970  addsprop  27972  addsuniflem  27997  mulsuniflem  28145  oncutlt  28260  oniso  28267  onsfi  28352  bdayn0p1  28365  addhalfcut  28455  tglowdim2ln  28723  axcontlem12  29048  elntg2  29058  numedglnl  29217  vtxd0nedgb  29562  wlkvtxedg  29717  pthd  29842  2pthdlem1  30003  clwlkclwwlk  30077  3pthdlem1  30239  frgrregord013  30470  grpoidinvlem3  30581  nmoubi  30847  lnon0  30873  adjsym  31908  nmopub  31983  nmfnleub  32000  cvbr2  32358  chpssati  32438  chrelat2i  32440  chrelat3  32446  mdsymlem8  32485  ralcom4f  32541  reuxfrdf  32565  n0nsnel  32590  uniinn0  32625  ssiun3  32633  disjnf  32645  disjorf  32654  disjunsn  32669  ac6sf2  32700  nn0min  32901  tosglblem  33056  archiabl  33280  1arithidom  33618  eulerpartlems  34517  eulerpartlemr  34531  eulerpartlemn  34538  ballotlem7  34693  bnj110  35014  bnj92  35018  bnj539  35047  bnj540  35048  bnj580  35069  bnj978  35105  bnj1047  35129  bnj1128  35146  bnj1417  35197  bnj1421  35198  bnj1312  35214  bnj1498  35217  onvf1od  35301  lfuhgr3  35314  subfacp1lem3  35376  cvmlift2lem1  35496  cvmlift2lem12  35508  satfv1  35557  fmlaomn0  35584  fmla0disjsuc  35592  fmlasucdisj  35593  untuni  35903  dfso3  35914  elintfv  35959  elpotr  35973  dfon2lem7  35981  dfon2lem9  35983  dfint3  36146  brlb  36149  filnetlem4  36575  regsfromregtr  36668  bj-reabeq  37228  ctbssinf  37611  fvineqsneq  37617  pibt2  37622  phpreu  37805  ptrecube  37821  poimirlem1  37822  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem30  37851  mblfinlem2  37859  ftc1anc  37902  inixp  37929  ac6gf  37933  heibor1lem  38010  heiborlem1  38012  iscrngo2  38198  ac6s3f  38372  ref5  38514  idinxpssinxp2  38519  n0elqs  38527  ineleq  38549  ralrnmo  38556  ssdmral  38574  refrelcosslem  38735  refrelcoss3  38736  lpssat  39283  lssat  39286  lcvbr2  39292  lcvbr3  39293  lfl1  39340  lub0N  39459  glb0N  39463  atlrelat1  39591  hlrelat2  39673  ispsubsp2  40016  pclclN  40161  cdleme25cv  40628  tendoeq2  41044  cdlemk35  41182  aks4d1p7  42347  sticksstones1  42410  indstrd  42457  supinf  42507  infdesc  42896  setindtrs  43277  unielss  43470  ssunib  43472  onsupmaxb  43491  onsupeqnmax  43499  cllem0  43817  ntrneixb  44346  gneispace  44385  expandral  44541  ismnuprim  44545  dfuniv2  44553  undisjrab  44557  zfregs2VD  45091  sswfaxreg  45238  dfac5prim  45241  permac8prim  45265  iindif2f  45414  ralfal  45415  disjinfi  45446  iuneqfzuz  45590  caucvgbf  45743  rexanuz2nf  45746  mccl  45854  limsupub  45958  limsuppnflem  45964  limsupre2lem  45978  lmbr3v  45999  liminfpnfuz  46070  xlimpnfxnegmnf2  46112  ioodvbdlimc1lem2  46186  ioodvbdlimc2lem  46188  dvnprodlem3  46202  fourierdlem103  46463  fourierdlem104  46464  sge0iunmpt  46672  meaiuninc3v  46738  hoidmvle  46854  issmff  46988  n0nsn2el  47281  r19.32  47354  2rexrsb  47358  cbvral2  47359  2reu3  47366  2reu8i  47369  otiunsndisjX  47535  0nelsetpreimafv  47646  dfgric2  48171  gpg5nbgrvtx03starlem1  48324  gpg5nbgrvtx03starlem2  48325  gpg5nbgrvtx03starlem3  48326  gpg5nbgrvtx13starlem1  48327  gpg5nbgrvtx13starlem2  48328  gpg5nbgrvtx13starlem3  48329  gpg5edgnedg  48386  copisnmnd  48425  lindslinindsimp1  48713  lindslinindsimp2  48719  snlindsntor  48727  ldepslinc  48765  iuneq0  49074  iinxp  49086  iscnrm3  49207  setrec1lem3  49944  aacllem  50056