Theorem ralbii 3109

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

This proof depends on syntax axioms:   ↔ wb 209   ∈ wcel 2145  ∀wral 3077

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3078

This theorem is used by:  dfral2  3114  ralinexa  3116  rexanali  3117  r19.26-3  3124  ralbiim  3125  2ralbii  3138  3ralbii  3140  4ralbii  3141  2ralbiim  3142  ralnex2  3143  nrexralim  3147  r19.26-2  3148  r19.23v  3190  r19.32v  3196  2ralor  3237  nelb  3239  cbvral2vw  3245  cbvral3vw  3247  ralrot3  3294  ralcom13  3295  sbralieALT  3340  cbvral2v  3354  cbvral3v  3356  ceqsralv  3491  ralxpxfr2d  3600  reu8  3691  2reuswap  3704  2reu5lem2  3714  2rmoswap  3719  rmoanim  3842  rmoanimALT  3843  dfdif3  4066  dfss5  4221  n0el  4312  ralnralall  4469  2reu4lem  4479  r19.12sn  4681  raldifsnb  4759  eqsn  4790  n0snor2el  4793  uni0b  4894  uni0c  4895  ssint  4924  iuniin  4964  iuneq2  4971  iunssf  5001  iunssfOLD  5002  iunss  5003  iunssOLD  5004  ssiinf  5013  iinab  5026  iinun2  5031  iindif1  5035  iindif2  5037  iinin2  5038  iinuni  5058  sspwuni  5060  iinpw  5066  disjor  5085  disjxun  5101  dftr3  5217  reusv3  5367  otiunsndisj  5493  ssrel2  5761  reliun  5794  xpiindi  5812  rexiunxp  5817  ralxpf  5824  rexxpf  5825  dfse2  6098  idrefALT  6107  asymref2  6111  rninxp  6171  dminxp  6172  cnviin  6289  cnvpo  6290  dfpo2  6299  dfse3  6339  frpoins2fg  6347  dffun9  6569  funcnv3  6610  fncnv  6613  fnres  6666  mptfnf  6674  fnopabg  6676  mptfng  6678  fint  6761  funimass4  6949  fndmdifeq0  7043  funconstss  7055  f1ompt  7111  idref  7149  fconstfv  7218  dff13f  7259  dff14b  7275  weniso  7364  fnssintima  7372  foov  7595  imaeqalov  7660  dfwe2  7788  tfis2f  7867  tfindes  7874  frxp  8138  ralxp3f  8154  frpoins3xpg  8157  frpoins3xp3g  8158  xpord2indlem  8164  xpord3inddlem  8171  soseq  8176  tz7.48lemOLD  8451  tz7.49  8455  oeordi  8596  naddcllem  8685  naddunif  8703  naddasslem2  8705  ixpeq2  8939  ixpin  8951  ixpiin  8952  boxriin  8968  findcard3  9274  fimax2g  9277  fissuni  9346  indexfi  9349  dfsup2  9436  sup0riota  9458  infcllem  9480  wemapsolem  9544  zfinf2  9643  oemapso  9683  ttrclresv  9718  zfregs2  9734  setinds  9750  setinds2f  9751  frins2f  9757  r1elss  9814  rankc1  9887  elhf4  9912  cp  9954  bnd2  9956  setrec1lem3  9969  aceq1  10196  aceq2  10198  kmlem7  10235  kmlem12  10240  kmlem13  10241  kmlem15  10243  fin12  10491  ac6num  10557  ac6s2  10564  ac6sf  10567  ac6s4  10568  zorn2lem4  10577  zorn2lem6  10579  zorn2lem7  10580  zorng  10582  ttukeylem6  10592  brdom7disj  10610  brdom6disj  10611  fpwwe2  10728  fpwwe  10731  axgroth5  10909  axgroth4  10917  grothprim  10919  nqereu  11014  dfinfre  12298  infrenegsup  12300  xrsupsslem  13437  xrinfmsslem  13438  xrinfmss2  13441  fzshftral  13749  fsuppmapnn0ub  14138  mptnn0fsuppr  14142  hashgt12el  14567  hashgt12el2  14568  hashbc  14598  s3iunsndisj  15121  cotr2g  15129  rexfiuz  15515  clim0  15673  rpnnen2lem12  16393  gcdcllem1  16669  absproddvds  16792  coprmproddvdslem  16837  vdwmc2  17157  vdwlem13  17171  vdwnn  17176  xpscf  17737  mreacs  17832  acsfn  17833  acsfn1  17835  acsfn2  17837  dfinito2  18178  dftermo2  18179  ispos2  18489  lublecllem  18532  odulub  18579  oduglb  18581  posglbdg  18587  isnmnd  18927  gsumwspan  19042  smndex2dnrinv  19114  isnsg2  19366  oppgid  19570  oppgcntz  19578  efgval2  19938  iscyggen2  20095  iscyg3  20100  dfring3  20518  oppr1  20580  isnirred  20650  isdomn5  20962  lssne0  21226  iunocv  21987  islindf4  22144  pmatcollpw2lem  23095  isbasis2g  23266  basdif0  23271  tgval2  23274  ntreq0  23395  isclo2  23406  opnnei  23438  neiptopnei  23450  lmres  23618  ist1-3  23667  cmpcov2  23708  cmpsub  23718  is1stc2  23760  1stccn  23782  kgencn  23875  eltx  23887  txkgen  23971  fbun  24159  trfbas  24163  fbunfip  24188  trfil2  24206  isufil2  24227  fixufil  24241  hausflim  24300  txflf  24325  fclsopn  24333  alexsubALTlem3  24368  isclmp  25418  iscau3  25599  iscau4  25600  caucfil  25604  bcth3  25652  ovolgelb  25801  dyadmax  25919  itg2leub  26055  itg2cn  26084  plydivex  26618  vieta1  26635  lgseisenlem2  27703  pnt3  27939  infdesc  27967  nosepon  28022  nomaxmo  28055  nosupbnd1lem4  28068  conway  28165  eqcuts2  28172  etaslts  28179  lesrec  28185  bday1  28200  cuteq1  28203  madebdaylemlrcut  28285  addsproplem4  28358  addsproplem6  28360  addsprop  28362  addsuniflem  28387  mulsuniflem  28535  oncutlt  28650  oniso  28657  onsfi  28742  bdayn0p1  28755  addhalfcut  28845  tglowdim2ln  29120  axcontlem12  29553  elntg2  29563  numedglnl  29722  lfuhgr3  29728  vtxd0nedgb  30069  wlkvtxedg  30224  pthd  30355  2pthdlem1  30519  clwlkclwwlk  30593  3pthdlem1  30765  frgrregord013  30996  grpoidinvlem3  31108  nmoubi  31374  lnon0  31400  adjsym  32435  nmopub  32510  nmfnleub  32527  cvbr2  32885  chpssati  32965  chrelat2i  32967  chrelat3  32973  mdsymlem8  33012  ralcom4f  33064  reuxfrdf  33087  n0nsnel  33111  uniinn0  33147  ssiun3  33153  disjnf  33164  disjorf  33173  disjunsn  33188  ac6sf2  33216  nn0min  33412  tosglblem  33535  archiabl  33759  1arithidom  34069  eulerpartlems  34992  eulerpartlemr  35006  eulerpartlemn  35013  ballotlem7  35168  bnj110  35488  bnj92  35492  bnj539  35521  bnj540  35522  bnj580  35543  bnj978  35579  bnj1047  35603  bnj1128  35620  bnj1417  35671  bnj1421  35672  bnj1312  35688  bnj1498  35691  r1omhf  35731  onvf1od  35886  subfacp1lem3  35947  cvmlift2lem1  36067  cvmlift2lem12  36079  satfv1  36128  fmlaomn0  36155  fmla0disjsuc  36163  fmlasucdisj  36164  untuni  36474  dfso3  36485  dffr5  36519  elintfv  36530  elpotr  36543  dfon2lem7  36551  dfon2lem9  36553  dfint3  36716  brlb  36719  dffr7  36720  filnetlem4  37169  axtco  37259  axtco1g  37264  regsfromregtco  37326  mh-infprim3bi  37336  bj-reabeq  37940  bj-axseprep  37990  ctbssinf  38329  fvineqsneq  38335  pibt2  38340  phpreu  38527  ptrecube  38538  poimirlem1  38539  poimirlem25  38563  poimirlem26  38564  poimirlem27  38565  poimirlem30  38568  mblfinlem2  38576  ftc1anc  38619  inixp  38662  ac6gf  38666  heibor1lem  38743  heiborlem1  38745  iscrngo2  38931  ac6s3f  39103  ref5  39251  idinxpssinxp2  39256  n0elqs  39264  ineleq  39286  ralrnmo  39293  ssdmral  39311  refrelcosslem  39484  refrelcoss3  39485  lpssat  40070  lssat  40073  lcvbr2  40079  lcvbr3  40080  lfl1  40127  lub0N  40246  glb0N  40250  atlrelat1  40378  hlrelat2  40460  ispsubsp2  40803  pclclN  40948  cdleme25cv  41415  tendoeq2  41831  cdlemk35  41969  aks4d1p7  43133  sticksstones1  43196  indstrd  43243  supinf  43293  frlmnzcoordex  43652  setindtrs  44031  unielss  44219  ssunib  44221  onsupmaxb  44240  onsupeqnmax  44248  cllem0  44566  ntrneixb  45094  gneispace  45133  expandral  45273  ismnuprim  45277  dfuniv2  45285  undisjrab  45289  zfregs2VD  45822  sswfaxreg  45976  dfac5prim  45979  permac8prim  46003  iindif2f  46174  ralfal  46175  disjinfi  46206  iuneqfzuz  46346  caucvgbf  46498  rexanuz2nf  46501  mccl  46609  limsupub  46713  limsuppnflem  46719  limsupre2lem  46733  lmbr3v  46754  liminfpnfuz  46825  xlimpnfxnegmnf2  46867  ioodvbdlimc1lem2  46941  ioodvbdlimc2lem  46943  dvnprodlem3  46957  fourierdlem103  47218  fourierdlem104  47219  sge0iunmpt  47427  meaiuninc3v  47493  hoidmvle  47609  issmff  47743  n0nsn2el  48094  r19.32  48167  2rexrsb  48171  cbvral2  48172  2reu3  48179  2reu8i  48182  otiunsndisjX  48348  0nelsetpreimafv  48471  dfgric2  49012  gpg5nbgrvtx03starlem1  49165  gpg5nbgrvtx03starlem2  49166  gpg5nbgrvtx03starlem3  49167  gpg5nbgrvtx13starlem1  49168  gpg5nbgrvtx13starlem2  49169  gpg5nbgrvtx13starlem3  49170  gpg5edgnedg  49227  copisnmnd  49265  lindslinindsimp1  49568  lindslinindsimp2  49574  snlindsntor  49582  ldepslinc  49620  iuneq0  49928  iinxp  49940  iscnrm3  50059  ralsbii  50896  ralseubii  50928  aacllem  50938