Theorem ralbii 3083

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

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

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

This theorem depends on definitions:  df-bi 207  df-ral 3052

This theorem is referenced by:  dfral2  3088  ralinexa  3090  rexanali  3091  r19.26-3  3098  ralbiim  3099  2ralbii  3112  3ralbii  3114  4ralbii  3115  2ralbiim  3116  ralnex2  3117  nrexralim  3121  r19.26-2  3122  r19.23v  3164  r19.32v  3170  2ralor  3211  nelb  3213  cbvral2vw  3219  cbvral3vw  3221  ralrot3  3268  ralcom13  3269  sbralieALT  3316  cbvral2v  3330  cbvral3v  3332  ceqsralv  3470  ralxpxfr2d  3588  reu8  3679  2reuswap  3692  2reu5lem2  3702  2rmoswap  3707  rmoanim  3832  rmoanimALT  3833  dfdif3  4057  dfss5  4215  n0el  4304  ralnralall  4453  2reu4lem  4463  r19.12sn  4664  raldifsnb  4741  eqsn  4772  n0snor2el  4776  uni0b  4876  uni0c  4877  ssint  4906  iuniin  4946  iuneq2  4953  iunssf  4985  iunssfOLD  4986  iunss  4987  iunssOLD  4988  ssiinf  4997  iinab  5010  iinun2  5015  iindif1  5017  iindif2  5019  iinin2  5020  iinuni  5040  sspwuni  5042  iinpw  5048  disjor  5067  disjxun  5083  dftr3  5197  reusv3  5347  otiunsndisj  5474  ssrel2  5741  reliun  5772  xpiindi  5790  rexiunxp  5795  ralxpf  5801  rexxpf  5802  dfse2  6065  idrefALT  6076  asymref2  6080  rninxp  6143  dminxp  6144  cnviin  6250  cnvpo  6251  dfpo2  6260  dfse3  6300  frpoins2fg  6308  dffun9  6527  funcnv3  6568  fncnv  6571  fnres  6625  mptfnf  6633  fnopabg  6635  mptfng  6637  fint  6719  funimass4  6904  fndmdifeq0  6996  funconstss  7008  f1ompt  7063  idref  7099  fconstfv  7167  dff13f  7210  dff14b  7226  weniso  7309  fnssintima  7317  foov  7541  imaeqalov  7606  dfwe2  7728  tfis2f  7807  tfindes  7814  frxp  8076  ralxp3f  8087  frpoins3xpg  8090  frpoins3xp3g  8091  xpord2indlem  8097  xpord3inddlem  8104  soseq  8109  tz7.48lem  8380  tz7.49  8384  oeordi  8523  naddcllem  8612  naddunif  8629  naddasslem2  8631  ixpeq2  8859  ixpin  8871  ixpiin  8872  boxriin  8888  findcard3  9193  fimax2g  9196  fissuni  9267  indexfi  9270  dfsup2  9357  sup0riota  9379  infcllem  9401  wemapsolem  9465  zfinf2  9563  oemapso  9603  ttrclresv  9638  zfregs2  9654  setinds  9670  setinds2f  9671  frins2f  9677  r1elss  9730  rankc1  9794  cp  9815  bnd2  9817  aceq1  10039  aceq2  10041  kmlem7  10079  kmlem12  10084  kmlem13  10085  kmlem15  10087  fin12  10335  ac6num  10401  ac6s2  10408  ac6sf  10411  ac6s4  10412  zorn2lem4  10421  zorn2lem6  10423  zorn2lem7  10424  zorng  10426  ttukeylem6  10436  brdom7disj  10453  brdom6disj  10454  fpwwe2  10566  fpwwe  10569  axgroth5  10747  axgroth4  10755  grothprim  10757  nqereu  10852  dfinfre  12137  infrenegsup  12139  xrsupsslem  13259  xrinfmsslem  13260  xrinfmss2  13263  fzshftral  13569  fsuppmapnn0ub  13957  mptnn0fsuppr  13961  hashgt12el  14384  hashgt12el2  14385  hashbc  14415  s3iunsndisj  14930  cotr2g  14938  rexfiuz  15310  clim0  15468  rpnnen2lem12  16192  gcdcllem1  16468  absproddvds  16586  coprmproddvdslem  16631  vdwmc2  16950  vdwlem13  16964  vdwnn  16969  xpscf  17529  mreacs  17624  acsfn  17625  acsfn1  17627  acsfn2  17629  dfinito2  17970  dftermo2  17971  ispos2  18281  lublecllem  18324  odulub  18371  oduglb  18373  posglbdg  18379  isnmnd  18706  gsumwspan  18814  smndex2dnrinv  18886  isnsg2  19131  oppgid  19331  oppgcntz  19339  efgval2  19699  iscyggen2  19856  iscyg3  19861  oppr1  20330  isnirred  20400  isdomn5  20687  isdomn2OLD  20689  lssne0  20946  iunocv  21661  islindf4  21818  pmatcollpw2lem  22742  isbasis2g  22913  basdif0  22918  tgval2  22921  ntreq0  23042  isclo2  23053  opnnei  23085  neiptopnei  23097  lmres  23265  ist1-3  23314  cmpcov2  23355  cmpsub  23365  is1stc2  23407  1stccn  23428  kgencn  23521  eltx  23533  txkgen  23617  fbun  23805  trfbas  23809  fbunfip  23834  trfil2  23852  isufil2  23873  fixufil  23887  hausflim  23946  txflf  23971  fclsopn  23979  alexsubALTlem3  24014  isclmp  25064  iscau3  25245  iscau4  25246  caucfil  25250  bcth3  25298  ovolgelb  25447  dyadmax  25565  itg2leub  25701  itg2cn  25730  plydivex  26263  vieta1  26278  lgseisenlem2  27339  pnt3  27575  nosepon  27629  nomaxmo  27662  nosupbnd1lem4  27675  conway  27771  eqcuts2  27778  etaslts  27785  lesrec  27791  bday1  27806  cuteq1  27809  madebdaylemlrcut  27891  addsproplem4  27964  addsproplem6  27966  addsprop  27968  addsuniflem  27993  mulsuniflem  28141  oncutlt  28256  oniso  28263  onsfi  28348  bdayn0p1  28361  addhalfcut  28451  tglowdim2ln  28719  axcontlem12  29044  elntg2  29054  numedglnl  29213  vtxd0nedgb  29557  wlkvtxedg  29712  pthd  29837  2pthdlem1  29998  clwlkclwwlk  30072  3pthdlem1  30234  frgrregord013  30465  grpoidinvlem3  30577  nmoubi  30843  lnon0  30869  adjsym  31904  nmopub  31979  nmfnleub  31996  cvbr2  32354  chpssati  32434  chrelat2i  32436  chrelat3  32442  mdsymlem8  32481  ralcom4f  32536  reuxfrdf  32560  n0nsnel  32585  uniinn0  32620  ssiun3  32628  disjnf  32640  disjorf  32649  disjunsn  32664  ac6sf2  32695  nn0min  32894  tosglblem  33034  archiabl  33259  1arithidom  33597  eulerpartlems  34504  eulerpartlemr  34518  eulerpartlemn  34525  ballotlem7  34680  bnj110  35000  bnj92  35004  bnj539  35033  bnj540  35034  bnj580  35055  bnj978  35091  bnj1047  35115  bnj1128  35132  bnj1417  35183  bnj1421  35184  bnj1312  35200  bnj1498  35203  onvf1od  35289  lfuhgr3  35302  subfacp1lem3  35364  cvmlift2lem1  35484  cvmlift2lem12  35496  satfv1  35545  fmlaomn0  35572  fmla0disjsuc  35580  fmlasucdisj  35581  untuni  35891  dfso3  35902  elintfv  35947  elpotr  35961  dfon2lem7  35969  dfon2lem9  35971  dfint3  36134  brlb  36137  filnetlem4  36563  axtco  36653  axtco1g  36658  regsfromregtco  36720  mh-infprim3bi  36730  bj-reabeq  37334  bj-axseprep  37381  ctbssinf  37722  fvineqsneq  37728  pibt2  37733  phpreu  37925  ptrecube  37941  poimirlem1  37942  poimirlem25  37966  poimirlem26  37967  poimirlem27  37968  poimirlem30  37971  mblfinlem2  37979  ftc1anc  38022  inixp  38049  ac6gf  38053  heibor1lem  38130  heiborlem1  38132  iscrngo2  38318  ac6s3f  38492  ref5  38640  idinxpssinxp2  38645  n0elqs  38653  ineleq  38675  ralrnmo  38682  ssdmral  38700  refrelcosslem  38873  refrelcoss3  38874  lpssat  39459  lssat  39462  lcvbr2  39468  lcvbr3  39469  lfl1  39516  lub0N  39635  glb0N  39639  atlrelat1  39767  hlrelat2  39849  ispsubsp2  40192  pclclN  40337  cdleme25cv  40804  tendoeq2  41220  cdlemk35  41358  aks4d1p7  42522  sticksstones1  42585  indstrd  42632  supinf  42681  infdesc  43076  setindtrs  43453  unielss  43646  ssunib  43648  onsupmaxb  43667  onsupeqnmax  43675  cllem0  43993  ntrneixb  44522  gneispace  44561  expandral  44717  ismnuprim  44721  dfuniv2  44729  undisjrab  44733  zfregs2VD  45267  sswfaxreg  45414  dfac5prim  45417  permac8prim  45441  iindif2f  45590  ralfal  45591  disjinfi  45622  iuneqfzuz  45765  caucvgbf  45917  rexanuz2nf  45920  mccl  46028  limsupub  46132  limsuppnflem  46138  limsupre2lem  46152  lmbr3v  46173  liminfpnfuz  46244  xlimpnfxnegmnf2  46286  ioodvbdlimc1lem2  46360  ioodvbdlimc2lem  46362  dvnprodlem3  46376  fourierdlem103  46637  fourierdlem104  46638  sge0iunmpt  46846  meaiuninc3v  46912  hoidmvle  47028  issmff  47162  n0nsn2el  47473  r19.32  47546  2rexrsb  47550  cbvral2  47551  2reu3  47558  2reu8i  47561  otiunsndisjX  47727  0nelsetpreimafv  47850  dfgric2  48391  gpg5nbgrvtx03starlem1  48544  gpg5nbgrvtx03starlem2  48545  gpg5nbgrvtx03starlem3  48546  gpg5nbgrvtx13starlem1  48547  gpg5nbgrvtx13starlem2  48548  gpg5nbgrvtx13starlem3  48549  gpg5edgnedg  48606  copisnmnd  48645  lindslinindsimp1  48933  lindslinindsimp2  48939  snlindsntor  48947  ldepslinc  48985  iuneq0  49294  iinxp  49306  iscnrm3  49427  setrec1lem3  50164  aacllem  50276