Theorem ralbii 3099

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

Syntax hints:   ↔ wb 206   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  dfral2  3105  ralinexa  3107  rexanali  3108  rexbiOLD  3111  r19.26-3  3118  ralbiim  3119  2ralbii  3134  3ralbii  3136  4ralbii  3137  2ralbiim  3138  ralnex2  3139  nrexralim  3143  r19.26-2  3144  r19.23v  3189  r19.32v  3198  2ralor  3237  nelb  3240  nelbOLD  3241  cbvral2vw  3247  cbvral3vw  3249  ralrot3  3299  ralcom13  3300  ralcom13OLD  3301  sbralieALT  3367  cbvral2v  3376  cbvral3v  3378  moelOLD  3413  ceqsralv  3531  ralxpxfr2d  3659  reu8  3755  2reuswap  3768  2reu5lem2  3778  2rmoswap  3783  rmoanim  3916  rmoanimALT  3917  dfdif3  4140  dfss5  4294  n0el  4387  ralnralall  4538  2reu4lem  4545  r19.12sn  4745  raldifsnb  4821  eqsn  4854  n0snor2el  4858  uni0b  4957  uni0c  4958  ssint  4988  iuniin  5027  iuneq2  5034  iunssf  5067  iunss  5068  ssiinf  5077  iinab  5091  iinun2  5096  iindif1  5098  iindif2  5100  iinin2  5101  iinuni  5121  sspwuni  5123  iinpw  5129  disjor  5148  disjxun  5164  dftr3  5289  reusv3  5423  otiunsndisj  5539  ssrel2  5809  reliun  5840  xpiindi  5860  rexiunxp  5865  ralxpf  5871  rexxpf  5872  dfse2  6130  idrefALT  6143  asymref2  6149  rninxp  6210  dminxp  6211  cnviin  6317  cnvpo  6318  dfpo2  6327  dfse3  6368  frpoins2fg  6376  wfis2fgOLD  6389  dffun9  6607  funcnv3  6648  fncnv  6651  fnres  6707  mptfnf  6715  fnopabg  6717  mptfng  6719  fint  6800  funimass4  6986  fndmdifeq0  7077  funconstss  7089  f1ompt  7145  idref  7180  fconstfv  7249  dff13f  7293  dff14b  7308  weniso  7390  fnssintima  7398  foov  7624  imaeqalov  7689  dfwe2  7809  tfis2f  7893  tfindes  7900  frxp  8167  ralxp3f  8178  frpoins3xpg  8181  frpoins3xp3g  8182  xpord2indlem  8188  xpord3inddlem  8195  soseq  8200  dfwrecsOLD  8354  tz7.48lem  8497  tz7.49  8501  oeordi  8643  naddcllem  8732  naddunif  8749  naddasslem2  8751  ixpeq2  8969  ixpin  8981  ixpiin  8982  boxriin  8998  findcard3  9346  findcard3OLD  9347  fimax2g  9350  fissuni  9427  indexfi  9430  dfsup2  9513  sup0riota  9534  infcllem  9556  wemapsolem  9619  zfinf2  9711  oemapso  9751  ttrclresv  9786  zfregs2  9802  frins2f  9822  r1elss  9875  rankc1  9939  cp  9960  bnd2  9962  aceq1  10186  aceq2  10188  kmlem7  10226  kmlem12  10231  kmlem13  10232  kmlem15  10234  fin12  10482  ac6num  10548  ac6s2  10555  ac6sf  10558  ac6s4  10559  zorn2lem4  10568  zorn2lem6  10570  zorn2lem7  10571  zorng  10573  ttukeylem6  10583  brdom7disj  10600  brdom6disj  10601  fpwwe2  10712  fpwwe  10715  axgroth5  10893  axgroth4  10901  grothprim  10903  nqereu  10998  dfinfre  12276  infrenegsup  12278  xrsupsslem  13369  xrinfmsslem  13370  xrinfmss2  13373  fzshftral  13672  fsuppmapnn0ub  14046  mptnn0fsuppr  14050  hashgt12el  14471  hashgt12el2  14472  hashbc  14502  s3iunsndisj  15017  cotr2g  15025  rexfiuz  15396  clim0  15552  rpnnen2lem12  16273  gcdcllem1  16545  absproddvds  16664  coprmproddvdslem  16709  vdwmc2  17026  vdwlem13  17040  vdwnn  17045  xpscf  17625  mreacs  17716  acsfn  17717  acsfn1  17719  acsfn2  17721  dfinito2  18070  dftermo2  18071  ispos2  18385  lublecllem  18430  odulub  18477  oduglb  18479  posglbdg  18485  isnmnd  18776  gsumwspan  18881  smndex2dnrinv  18950  isnsg2  19196  oppgid  19399  oppgcntz  19407  efgval2  19766  iscyggen2  19923  iscyg3  19928  oppr1  20376  isnirred  20446  isdomn5  20732  isdomn2OLD  20734  lssne0  20972  iunocv  21722  islindf4  21881  pmatcollpw2lem  22804  isbasis2g  22976  basdif0  22981  tgval2  22984  ntreq0  23106  isclo2  23117  opnnei  23149  neiptopnei  23161  lmres  23329  ist1-3  23378  cmpcov2  23419  cmpsub  23429  is1stc2  23471  1stccn  23492  kgencn  23585  eltx  23597  txkgen  23681  fbun  23869  trfbas  23873  fbunfip  23898  trfil2  23916  isufil2  23937  fixufil  23951  hausflim  24010  txflf  24035  fclsopn  24043  alexsubALTlem3  24078  isclmp  25149  iscau3  25331  iscau4  25332  caucfil  25336  bcth3  25384  ovolgelb  25534  dyadmax  25652  itg2leub  25789  itg2cn  25818  plydivex  26357  vieta1  26372  lgseisenlem2  27438  pnt3  27674  nosepon  27728  nomaxmo  27761  nosupbnd1lem4  27774  conway  27862  eqscut2  27869  etasslt  27876  slerec  27882  bday1s  27894  cuteq1  27896  madebdaylemlrcut  27955  addsproplem4  28023  addsproplem6  28025  addsprop  28027  addsuniflem  28052  mulsuniflem  28193  halfcut  28434  addhalfcut  28437  tglowdim2ln  28677  axcontlem12  29008  elntg2  29018  numedglnl  29179  vtxd0nedgb  29524  wlkvtxedg  29680  pthd  29805  2pthdlem1  29963  clwlkclwwlk  30034  3pthdlem1  30196  frgrregord013  30427  grpoidinvlem3  30538  nmoubi  30804  lnon0  30830  adjsym  31865  nmopub  31940  nmfnleub  31957  cvbr2  32315  chpssati  32395  chrelat2i  32397  chrelat3  32403  mdsymlem8  32442  ralcom4f  32496  reuxfrdf  32519  n0nsnel  32544  uniinn0  32573  ssiun3  32581  disjnf  32592  disjorf  32601  disjunsn  32616  ac6sf2  32644  nn0min  32824  tosglblem  32947  archiabl  33178  1arithidom  33530  eulerpartlems  34325  eulerpartlemr  34339  eulerpartlemn  34346  ballotlem7  34500  bnj110  34834  bnj92  34838  bnj539  34867  bnj540  34868  bnj580  34889  bnj978  34925  bnj1047  34949  bnj1128  34966  bnj1417  35017  bnj1421  35018  bnj1312  35034  bnj1498  35037  lfuhgr3  35087  subfacp1lem3  35150  cvmlift2lem1  35270  cvmlift2lem12  35282  satfv1  35331  fmlaomn0  35358  fmla0disjsuc  35366  fmlasucdisj  35367  untuni  35671  dfso3  35682  elintfv  35728  setinds  35742  setinds2f  35743  elpotr  35745  dfon2lem7  35753  dfon2lem9  35755  dfint3  35916  brlb  35919  filnetlem4  36347  bj-reabeq  36993  ctbssinf  37372  fvineqsneq  37378  pibt2  37383  phpreu  37564  ptrecube  37580  poimirlem1  37581  poimirlem25  37605  poimirlem26  37606  poimirlem27  37607  poimirlem30  37610  mblfinlem2  37618  ftc1anc  37661  inixp  37688  ac6gf  37692  heibor1lem  37769  heiborlem1  37771  iscrngo2  37957  ac6s3f  38131  ref5  38269  idinxpssinxp2  38274  n0elqs  38282  ineleq  38310  refrelcosslem  38418  refrelcoss3  38419  lpssat  38969  lssat  38972  lcvbr2  38978  lcvbr3  38979  lfl1  39026  lub0N  39145  glb0N  39149  atlrelat1  39277  hlrelat2  39360  ispsubsp2  39703  pclclN  39848  cdleme25cv  40315  tendoeq2  40731  cdlemk35  40869  aks4d1p7  42040  sticksstones1  42103  indstrd  42150  supinf  42237  infdesc  42598  setindtrs  42982  unielss  43179  ssunib  43181  onsupmaxb  43200  onsupeqnmax  43208  cllem0  43528  ntrneixb  44057  gneispace  44096  expandral  44259  ismnuprim  44263  dfuniv2  44271  undisjrab  44275  zfregs2VD  44812  iindif2f  45065  ralfal  45066  disjinfi  45099  iuneqfzuz  45250  caucvgbf  45405  rexanuz2nf  45408  mccl  45519  limsupub  45625  limsuppnflem  45631  limsupre2lem  45645  lmbr3v  45666  liminfpnfuz  45737  xlimpnfxnegmnf2  45779  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem3  45869  fourierdlem103  46130  fourierdlem104  46131  sge0iunmpt  46339  meaiuninc3v  46405  hoidmvle  46521  issmff  46655  n0nsn2el  46940  r19.32  47013  2rexrsb  47017  cbvral2  47018  2reu3  47025  2reu8i  47028  otiunsndisjX  47194  0nelsetpreimafv  47264  dfgric2  47768  copisnmnd  47892  lindslinindsimp1  48186  lindslinindsimp2  48192  snlindsntor  48200  ldepslinc  48238  iscnrm3  48632  setrec1lem3  48781  aacllem  48895