Theorem ralbii 3075

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

Syntax hints:   ↔ wb 206   ∈ wcel 2109  ∀wral 3044

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 3045

This theorem is referenced by:  dfral2  3081  ralinexa  3083  rexanali  3084  r19.26-3  3092  ralbiim  3093  2ralbii  3108  3ralbii  3110  4ralbii  3111  2ralbiim  3112  ralnex2  3113  nrexralim  3117  r19.26-2  3118  r19.23v  3160  r19.32v  3168  2ralor  3209  nelb  3211  cbvral2vw  3217  cbvral3vw  3219  ralrot3  3266  ralcom13  3267  ralcom13OLD  3268  sbralieALT  3324  cbvral2v  3339  cbvral3v  3341  ceqsralv  3485  ralxpxfr2d  3609  reu8  3701  2reuswap  3714  2reu5lem2  3724  2rmoswap  3729  rmoanim  3854  rmoanimALT  3855  dfdif3  4076  dfss5  4234  n0el  4323  ralnralall  4474  2reu4lem  4481  r19.12sn  4680  raldifsnb  4756  eqsn  4789  n0snor2el  4793  uni0b  4893  uni0c  4894  ssint  4924  iuniin  4964  iuneq2  4971  iunssf  5003  iunss  5004  ssiinf  5013  iinab  5027  iinun2  5032  iindif1  5034  iindif2  5036  iinin2  5037  iinuni  5057  sspwuni  5059  iinpw  5065  disjor  5084  disjxun  5100  dftr3  5215  reusv3  5355  otiunsndisj  5475  ssrel2  5739  reliun  5770  xpiindi  5789  rexiunxp  5794  ralxpf  5800  rexxpf  5801  dfse2  6060  idrefALT  6072  asymref2  6078  rninxp  6140  dminxp  6141  cnviin  6247  cnvpo  6248  dfpo2  6257  dfse3  6297  frpoins2fg  6305  dffun9  6529  funcnv3  6570  fncnv  6573  fnres  6627  mptfnf  6635  fnopabg  6637  mptfng  6639  fint  6721  funimass4  6907  fndmdifeq0  6998  funconstss  7010  f1ompt  7065  idref  7100  fconstfv  7168  dff13f  7212  dff14b  7228  weniso  7311  fnssintima  7319  foov  7543  imaeqalov  7608  dfwe2  7730  tfis2f  7812  tfindes  7819  frxp  8082  ralxp3f  8093  frpoins3xpg  8096  frpoins3xp3g  8097  xpord2indlem  8103  xpord3inddlem  8110  soseq  8115  tz7.48lem  8386  tz7.49  8390  oeordi  8528  naddcllem  8617  naddunif  8634  naddasslem2  8636  ixpeq2  8861  ixpin  8873  ixpiin  8874  boxriin  8890  findcard3  9205  findcard3OLD  9206  fimax2g  9209  fissuni  9284  indexfi  9287  dfsup2  9371  sup0riota  9393  infcllem  9415  wemapsolem  9479  zfinf2  9571  oemapso  9611  ttrclresv  9646  zfregs2  9662  frins2f  9682  r1elss  9735  rankc1  9799  cp  9820  bnd2  9822  aceq1  10046  aceq2  10048  kmlem7  10086  kmlem12  10091  kmlem13  10092  kmlem15  10094  fin12  10342  ac6num  10408  ac6s2  10415  ac6sf  10418  ac6s4  10419  zorn2lem4  10428  zorn2lem6  10430  zorn2lem7  10431  zorng  10433  ttukeylem6  10443  brdom7disj  10460  brdom6disj  10461  fpwwe2  10572  fpwwe  10575  axgroth5  10753  axgroth4  10761  grothprim  10763  nqereu  10858  dfinfre  12140  infrenegsup  12142  xrsupsslem  13243  xrinfmsslem  13244  xrinfmss2  13247  fzshftral  13552  fsuppmapnn0ub  13936  mptnn0fsuppr  13940  hashgt12el  14363  hashgt12el2  14364  hashbc  14394  s3iunsndisj  14910  cotr2g  14918  rexfiuz  15290  clim0  15448  rpnnen2lem12  16169  gcdcllem1  16445  absproddvds  16563  coprmproddvdslem  16608  vdwmc2  16926  vdwlem13  16940  vdwnn  16945  xpscf  17504  mreacs  17599  acsfn  17600  acsfn1  17602  acsfn2  17604  dfinito2  17945  dftermo2  17946  ispos2  18256  lublecllem  18299  odulub  18346  oduglb  18348  posglbdg  18354  isnmnd  18647  gsumwspan  18755  smndex2dnrinv  18824  isnsg2  19070  oppgid  19270  oppgcntz  19278  efgval2  19638  iscyggen2  19795  iscyg3  19800  oppr1  20270  isnirred  20340  isdomn5  20630  isdomn2OLD  20632  lssne0  20889  iunocv  21623  islindf4  21780  pmatcollpw2lem  22697  isbasis2g  22868  basdif0  22873  tgval2  22876  ntreq0  22997  isclo2  23008  opnnei  23040  neiptopnei  23052  lmres  23220  ist1-3  23269  cmpcov2  23310  cmpsub  23320  is1stc2  23362  1stccn  23383  kgencn  23476  eltx  23488  txkgen  23572  fbun  23760  trfbas  23764  fbunfip  23789  trfil2  23807  isufil2  23828  fixufil  23842  hausflim  23901  txflf  23926  fclsopn  23934  alexsubALTlem3  23969  isclmp  25030  iscau3  25211  iscau4  25212  caucfil  25216  bcth3  25264  ovolgelb  25414  dyadmax  25532  itg2leub  25668  itg2cn  25697  plydivex  26238  vieta1  26253  lgseisenlem2  27320  pnt3  27556  nosepon  27610  nomaxmo  27643  nosupbnd1lem4  27656  conway  27745  eqscut2  27752  etasslt  27759  slerec  27765  bday1s  27780  cuteq1  27783  madebdaylemlrcut  27848  addsproplem4  27919  addsproplem6  27921  addsprop  27923  addsuniflem  27948  mulsuniflem  28092  onscutlt  28205  onsiso  28209  onsfi  28287  bdayn0p1  28298  addhalfcut  28382  tglowdim2ln  28631  axcontlem12  28955  elntg2  28965  numedglnl  29124  vtxd0nedgb  29469  wlkvtxedg  29624  pthd  29749  2pthdlem1  29910  clwlkclwwlk  29981  3pthdlem1  30143  frgrregord013  30374  grpoidinvlem3  30485  nmoubi  30751  lnon0  30777  adjsym  31812  nmopub  31887  nmfnleub  31904  cvbr2  32262  chpssati  32342  chrelat2i  32344  chrelat3  32350  mdsymlem8  32389  ralcom4f  32446  reuxfrdf  32470  n0nsnel  32494  uniinn0  32529  ssiun3  32537  disjnf  32549  disjorf  32558  disjunsn  32573  ac6sf2  32598  nn0min  32795  tosglblem  32946  archiabl  33167  1arithidom  33501  eulerpartlems  34344  eulerpartlemr  34358  eulerpartlemn  34365  ballotlem7  34520  bnj110  34841  bnj92  34845  bnj539  34874  bnj540  34875  bnj580  34896  bnj978  34932  bnj1047  34956  bnj1128  34973  bnj1417  35024  bnj1421  35025  bnj1312  35041  bnj1498  35044  onvf1od  35087  lfuhgr3  35100  subfacp1lem3  35162  cvmlift2lem1  35282  cvmlift2lem12  35294  satfv1  35343  fmlaomn0  35370  fmla0disjsuc  35378  fmlasucdisj  35379  untuni  35689  dfso3  35700  elintfv  35745  setinds  35759  setinds2f  35760  elpotr  35762  dfon2lem7  35770  dfon2lem9  35772  dfint3  35933  brlb  35936  filnetlem4  36362  bj-reabeq  37008  ctbssinf  37387  fvineqsneq  37393  pibt2  37398  phpreu  37591  ptrecube  37607  poimirlem1  37608  poimirlem25  37632  poimirlem26  37633  poimirlem27  37634  poimirlem30  37637  mblfinlem2  37645  ftc1anc  37688  inixp  37715  ac6gf  37719  heibor1lem  37796  heiborlem1  37798  iscrngo2  37984  ac6s3f  38158  ref5  38294  idinxpssinxp2  38299  n0elqs  38307  ineleq  38329  refrelcosslem  38446  refrelcoss3  38447  lpssat  38999  lssat  39002  lcvbr2  39008  lcvbr3  39009  lfl1  39056  lub0N  39175  glb0N  39179  atlrelat1  39307  hlrelat2  39390  ispsubsp2  39733  pclclN  39878  cdleme25cv  40345  tendoeq2  40761  cdlemk35  40899  aks4d1p7  42064  sticksstones1  42127  indstrd  42174  supinf  42223  infdesc  42624  setindtrs  43007  unielss  43200  ssunib  43202  onsupmaxb  43221  onsupeqnmax  43229  cllem0  43548  ntrneixb  44077  gneispace  44116  expandral  44272  ismnuprim  44276  dfuniv2  44284  undisjrab  44288  zfregs2VD  44823  sswfaxreg  44970  dfac5prim  44973  permac8prim  44997  iindif2f  45147  ralfal  45148  disjinfi  45179  iuneqfzuz  45324  caucvgbf  45478  rexanuz2nf  45481  mccl  45589  limsupub  45695  limsuppnflem  45701  limsupre2lem  45715  lmbr3v  45736  liminfpnfuz  45807  xlimpnfxnegmnf2  45849  ioodvbdlimc1lem2  45923  ioodvbdlimc2lem  45925  dvnprodlem3  45939  fourierdlem103  46200  fourierdlem104  46201  sge0iunmpt  46409  meaiuninc3v  46475  hoidmvle  46591  issmff  46725  n0nsn2el  47019  r19.32  47092  2rexrsb  47096  cbvral2  47097  2reu3  47104  2reu8i  47107  otiunsndisjX  47273  0nelsetpreimafv  47384  dfgric2  47908  gpg5nbgrvtx03starlem1  48052  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx03starlem3  48054  gpg5nbgrvtx13starlem1  48055  gpg5nbgrvtx13starlem2  48056  gpg5nbgrvtx13starlem3  48057  copisnmnd  48150  lindslinindsimp1  48439  lindslinindsimp2  48445  snlindsntor  48453  ldepslinc  48491  iuneq0  48800  iinxp  48812  iscnrm3  48933  setrec1lem3  49671  aacllem  49783