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 2108  ∀wral 3051

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

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  3099  ralbiim  3100  2ralbii  3115  3ralbii  3117  4ralbii  3118  2ralbiim  3119  ralnex2  3120  nrexralim  3124  r19.26-2  3125  r19.23v  3168  r19.32v  3177  2ralor  3215  nelb  3218  cbvral2vw  3224  cbvral3vw  3226  ralrot3  3274  ralcom13  3275  ralcom13OLD  3276  sbralieALT  3338  cbvral2v  3347  cbvral3v  3349  moelOLD  3384  ceqsralv  3501  ralxpxfr2d  3625  reu8  3716  2reuswap  3729  2reu5lem2  3739  2rmoswap  3744  rmoanim  3869  rmoanimALT  3870  dfdif3  4092  dfss5  4250  n0el  4339  ralnralall  4490  2reu4lem  4497  r19.12sn  4696  raldifsnb  4772  eqsn  4805  n0snor2el  4809  uni0b  4909  uni0c  4910  ssint  4940  iuniin  4980  iuneq2  4987  iunssf  5020  iunss  5021  ssiinf  5030  iinab  5044  iinun2  5049  iindif1  5051  iindif2  5053  iinin2  5054  iinuni  5074  sspwuni  5076  iinpw  5082  disjor  5101  disjxun  5117  dftr3  5235  reusv3  5375  otiunsndisj  5495  ssrel2  5764  reliun  5795  xpiindi  5815  rexiunxp  5820  ralxpf  5826  rexxpf  5827  dfse2  6087  idrefALT  6100  asymref2  6106  rninxp  6168  dminxp  6169  cnviin  6275  cnvpo  6276  dfpo2  6285  dfse3  6325  frpoins2fg  6333  wfis2fgOLD  6346  dffun9  6564  funcnv3  6605  fncnv  6608  fnres  6664  mptfnf  6672  fnopabg  6674  mptfng  6676  fint  6756  funimass4  6942  fndmdifeq0  7033  funconstss  7045  f1ompt  7100  idref  7135  fconstfv  7203  dff13f  7247  dff14b  7263  weniso  7346  fnssintima  7354  foov  7579  imaeqalov  7644  dfwe2  7766  tfis2f  7849  tfindes  7856  frxp  8123  ralxp3f  8134  frpoins3xpg  8137  frpoins3xp3g  8138  xpord2indlem  8144  xpord3inddlem  8151  soseq  8156  dfwrecsOLD  8310  tz7.48lem  8453  tz7.49  8457  oeordi  8597  naddcllem  8686  naddunif  8703  naddasslem2  8705  ixpeq2  8923  ixpin  8935  ixpiin  8936  boxriin  8952  findcard3  9288  findcard3OLD  9289  fimax2g  9292  fissuni  9367  indexfi  9370  dfsup2  9454  sup0riota  9476  infcllem  9498  wemapsolem  9562  zfinf2  9654  oemapso  9694  ttrclresv  9729  zfregs2  9745  frins2f  9765  r1elss  9818  rankc1  9882  cp  9903  bnd2  9905  aceq1  10129  aceq2  10131  kmlem7  10169  kmlem12  10174  kmlem13  10175  kmlem15  10177  fin12  10425  ac6num  10491  ac6s2  10498  ac6sf  10501  ac6s4  10502  zorn2lem4  10511  zorn2lem6  10513  zorn2lem7  10514  zorng  10516  ttukeylem6  10526  brdom7disj  10543  brdom6disj  10544  fpwwe2  10655  fpwwe  10658  axgroth5  10836  axgroth4  10844  grothprim  10846  nqereu  10941  dfinfre  12221  infrenegsup  12223  xrsupsslem  13321  xrinfmsslem  13322  xrinfmss2  13325  fzshftral  13630  fsuppmapnn0ub  14011  mptnn0fsuppr  14015  hashgt12el  14438  hashgt12el2  14439  hashbc  14469  s3iunsndisj  14985  cotr2g  14993  rexfiuz  15364  clim0  15520  rpnnen2lem12  16241  gcdcllem1  16516  absproddvds  16634  coprmproddvdslem  16679  vdwmc2  16997  vdwlem13  17011  vdwnn  17016  xpscf  17577  mreacs  17668  acsfn  17669  acsfn1  17671  acsfn2  17673  dfinito2  18014  dftermo2  18015  ispos2  18325  lublecllem  18368  odulub  18415  oduglb  18417  posglbdg  18423  isnmnd  18714  gsumwspan  18822  smndex2dnrinv  18891  isnsg2  19137  oppgid  19337  oppgcntz  19345  efgval2  19703  iscyggen2  19860  iscyg3  19865  oppr1  20308  isnirred  20378  isdomn5  20668  isdomn2OLD  20670  lssne0  20906  iunocv  21639  islindf4  21796  pmatcollpw2lem  22713  isbasis2g  22884  basdif0  22889  tgval2  22892  ntreq0  23013  isclo2  23024  opnnei  23056  neiptopnei  23068  lmres  23236  ist1-3  23285  cmpcov2  23326  cmpsub  23336  is1stc2  23378  1stccn  23399  kgencn  23492  eltx  23504  txkgen  23588  fbun  23776  trfbas  23780  fbunfip  23805  trfil2  23823  isufil2  23844  fixufil  23858  hausflim  23917  txflf  23942  fclsopn  23950  alexsubALTlem3  23985  isclmp  25046  iscau3  25228  iscau4  25229  caucfil  25233  bcth3  25281  ovolgelb  25431  dyadmax  25549  itg2leub  25685  itg2cn  25714  plydivex  26255  vieta1  26270  lgseisenlem2  27337  pnt3  27573  nosepon  27627  nomaxmo  27660  nosupbnd1lem4  27673  conway  27761  eqscut2  27768  etasslt  27775  slerec  27781  bday1s  27793  cuteq1  27795  madebdaylemlrcut  27854  addsproplem4  27922  addsproplem6  27924  addsprop  27926  addsuniflem  27951  mulsuniflem  28092  halfcut  28333  addhalfcut  28336  tglowdim2ln  28576  axcontlem12  28900  elntg2  28910  numedglnl  29069  vtxd0nedgb  29414  wlkvtxedg  29570  pthd  29697  2pthdlem1  29858  clwlkclwwlk  29929  3pthdlem1  30091  frgrregord013  30322  grpoidinvlem3  30433  nmoubi  30699  lnon0  30725  adjsym  31760  nmopub  31835  nmfnleub  31852  cvbr2  32210  chpssati  32290  chrelat2i  32292  chrelat3  32298  mdsymlem8  32337  ralcom4f  32394  reuxfrdf  32418  n0nsnel  32442  uniinn0  32477  ssiun3  32485  disjnf  32497  disjorf  32506  disjunsn  32521  ac6sf2  32548  nn0min  32745  tosglblem  32900  archiabl  33142  1arithidom  33498  eulerpartlems  34338  eulerpartlemr  34352  eulerpartlemn  34359  ballotlem7  34514  bnj110  34835  bnj92  34839  bnj539  34868  bnj540  34869  bnj580  34890  bnj978  34926  bnj1047  34950  bnj1128  34967  bnj1417  35018  bnj1421  35019  bnj1312  35035  bnj1498  35038  lfuhgr3  35088  subfacp1lem3  35150  cvmlift2lem1  35270  cvmlift2lem12  35282  satfv1  35331  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  untuni  35672  dfso3  35683  elintfv  35728  setinds  35742  setinds2f  35743  elpotr  35745  dfon2lem7  35753  dfon2lem9  35755  dfint3  35916  brlb  35919  filnetlem4  36345  bj-reabeq  36991  ctbssinf  37370  fvineqsneq  37376  pibt2  37381  phpreu  37574  ptrecube  37590  poimirlem1  37591  poimirlem25  37615  poimirlem26  37616  poimirlem27  37617  poimirlem30  37620  mblfinlem2  37628  ftc1anc  37671  inixp  37698  ac6gf  37702  heibor1lem  37779  heiborlem1  37781  iscrngo2  37967  ac6s3f  38141  ref5  38277  idinxpssinxp2  38282  n0elqs  38290  ineleq  38318  refrelcosslem  38426  refrelcoss3  38427  lpssat  38977  lssat  38980  lcvbr2  38986  lcvbr3  38987  lfl1  39034  lub0N  39153  glb0N  39157  atlrelat1  39285  hlrelat2  39368  ispsubsp2  39711  pclclN  39856  cdleme25cv  40323  tendoeq2  40739  cdlemk35  40877  aks4d1p7  42042  sticksstones1  42105  indstrd  42152  supinf  42240  infdesc  42613  setindtrs  42996  unielss  43189  ssunib  43191  onsupmaxb  43210  onsupeqnmax  43218  cllem0  43537  ntrneixb  44066  gneispace  44105  expandral  44262  ismnuprim  44266  dfuniv2  44274  undisjrab  44278  zfregs2VD  44813  sswfaxreg  44960  dfac5prim  44963  iindif2f  45132  ralfal  45133  disjinfi  45164  iuneqfzuz  45310  caucvgbf  45464  rexanuz2nf  45467  mccl  45575  limsupub  45681  limsuppnflem  45687  limsupre2lem  45701  lmbr3v  45722  liminfpnfuz  45793  xlimpnfxnegmnf2  45835  ioodvbdlimc1lem2  45909  ioodvbdlimc2lem  45911  dvnprodlem3  45925  fourierdlem103  46186  fourierdlem104  46187  sge0iunmpt  46395  meaiuninc3v  46461  hoidmvle  46577  issmff  46711  n0nsn2el  47002  r19.32  47075  2rexrsb  47079  cbvral2  47080  2reu3  47087  2reu8i  47090  otiunsndisjX  47256  0nelsetpreimafv  47352  dfgric2  47876  gpg5nbgrvtx03starlem1  48018  gpg5nbgrvtx03starlem2  48019  gpg5nbgrvtx03starlem3  48020  gpg5nbgrvtx13starlem1  48021  gpg5nbgrvtx13starlem2  48022  gpg5nbgrvtx13starlem3  48023  copisnmnd  48092  lindslinindsimp1  48381  lindslinindsimp2  48387  snlindsntor  48395  ldepslinc  48433  iuneq0  48745  iinxp  48757  iscnrm3  48874  setrec1lem3  49501  aacllem  49613