Theorem ralbii 3078

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

Syntax hints:   ↔ wb 206   ∈ wcel 2111  ∀wral 3047

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

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

This theorem is referenced by:  dfral2  3083  ralinexa  3085  rexanali  3086  r19.26-3  3093  ralbiim  3094  2ralbii  3107  3ralbii  3109  4ralbii  3110  2ralbiim  3111  ralnex2  3112  nrexralim  3116  r19.26-2  3117  r19.23v  3159  r19.32v  3165  2ralor  3206  nelb  3208  cbvral2vw  3214  cbvral3vw  3216  ralrot3  3263  ralcom13  3264  sbralieALT  3319  cbvral2v  3334  cbvral3v  3336  ceqsralv  3477  ralxpxfr2d  3596  reu8  3687  2reuswap  3700  2reu5lem2  3710  2rmoswap  3715  rmoanim  3840  rmoanimALT  3841  dfdif3  4064  dfss5  4222  n0el  4311  ralnralall  4462  2reu4lem  4469  r19.12sn  4670  raldifsnb  4745  eqsn  4778  n0snor2el  4782  uni0b  4882  uni0c  4883  ssint  4912  iuniin  4952  iuneq2  4959  iunssf  4991  iunss  4992  ssiinf  5001  iinab  5014  iinun2  5019  iindif1  5021  iindif2  5023  iinin2  5024  iinuni  5044  sspwuni  5046  iinpw  5052  disjor  5071  disjxun  5087  dftr3  5201  reusv3  5341  otiunsndisj  5458  ssrel2  5724  reliun  5755  xpiindi  5774  rexiunxp  5779  ralxpf  5785  rexxpf  5786  dfse2  6048  idrefALT  6059  asymref2  6063  rninxp  6126  dminxp  6127  cnviin  6233  cnvpo  6234  dfpo2  6243  dfse3  6283  frpoins2fg  6291  dffun9  6510  funcnv3  6551  fncnv  6554  fnres  6608  mptfnf  6616  fnopabg  6618  mptfng  6620  fint  6702  funimass4  6886  fndmdifeq0  6977  funconstss  6989  f1ompt  7044  idref  7079  fconstfv  7146  dff13f  7189  dff14b  7205  weniso  7288  fnssintima  7296  foov  7520  imaeqalov  7585  dfwe2  7707  tfis2f  7786  tfindes  7793  frxp  8056  ralxp3f  8067  frpoins3xpg  8070  frpoins3xp3g  8071  xpord2indlem  8077  xpord3inddlem  8084  soseq  8089  tz7.48lem  8360  tz7.49  8364  oeordi  8502  naddcllem  8591  naddunif  8608  naddasslem2  8610  ixpeq2  8835  ixpin  8847  ixpiin  8848  boxriin  8864  findcard3  9167  fimax2g  9170  fissuni  9241  indexfi  9244  dfsup2  9328  sup0riota  9350  infcllem  9372  wemapsolem  9436  zfinf2  9532  oemapso  9572  ttrclresv  9607  zfregs2  9623  setinds  9639  setinds2f  9640  frins2f  9646  r1elss  9699  rankc1  9763  cp  9784  bnd2  9786  aceq1  10008  aceq2  10010  kmlem7  10048  kmlem12  10053  kmlem13  10054  kmlem15  10056  fin12  10304  ac6num  10370  ac6s2  10377  ac6sf  10380  ac6s4  10381  zorn2lem4  10390  zorn2lem6  10392  zorn2lem7  10393  zorng  10395  ttukeylem6  10405  brdom7disj  10422  brdom6disj  10423  fpwwe2  10534  fpwwe  10537  axgroth5  10715  axgroth4  10723  grothprim  10725  nqereu  10820  dfinfre  12103  infrenegsup  12105  xrsupsslem  13206  xrinfmsslem  13207  xrinfmss2  13210  fzshftral  13515  fsuppmapnn0ub  13902  mptnn0fsuppr  13906  hashgt12el  14329  hashgt12el2  14330  hashbc  14360  s3iunsndisj  14875  cotr2g  14883  rexfiuz  15255  clim0  15413  rpnnen2lem12  16134  gcdcllem1  16410  absproddvds  16528  coprmproddvdslem  16573  vdwmc2  16891  vdwlem13  16905  vdwnn  16910  xpscf  17469  mreacs  17564  acsfn  17565  acsfn1  17567  acsfn2  17569  dfinito2  17910  dftermo2  17911  ispos2  18221  lublecllem  18264  odulub  18311  oduglb  18313  posglbdg  18319  isnmnd  18646  gsumwspan  18754  smndex2dnrinv  18823  isnsg2  19068  oppgid  19268  oppgcntz  19276  efgval2  19636  iscyggen2  19793  iscyg3  19798  oppr1  20268  isnirred  20338  isdomn5  20625  isdomn2OLD  20627  lssne0  20884  iunocv  21618  islindf4  21775  pmatcollpw2lem  22692  isbasis2g  22863  basdif0  22868  tgval2  22871  ntreq0  22992  isclo2  23003  opnnei  23035  neiptopnei  23047  lmres  23215  ist1-3  23264  cmpcov2  23305  cmpsub  23315  is1stc2  23357  1stccn  23378  kgencn  23471  eltx  23483  txkgen  23567  fbun  23755  trfbas  23759  fbunfip  23784  trfil2  23802  isufil2  23823  fixufil  23837  hausflim  23896  txflf  23921  fclsopn  23929  alexsubALTlem3  23964  isclmp  25024  iscau3  25205  iscau4  25206  caucfil  25210  bcth3  25258  ovolgelb  25408  dyadmax  25526  itg2leub  25662  itg2cn  25691  plydivex  26232  vieta1  26247  lgseisenlem2  27314  pnt3  27550  nosepon  27604  nomaxmo  27637  nosupbnd1lem4  27650  conway  27740  eqscut2  27747  etasslt  27754  slerec  27760  bday1s  27775  cuteq1  27778  madebdaylemlrcut  27844  addsproplem4  27915  addsproplem6  27917  addsprop  27919  addsuniflem  27944  mulsuniflem  28088  onscutlt  28201  onsiso  28205  onsfi  28283  bdayn0p1  28294  addhalfcut  28379  tglowdim2ln  28629  axcontlem12  28953  elntg2  28963  numedglnl  29122  vtxd0nedgb  29467  wlkvtxedg  29622  pthd  29747  2pthdlem1  29908  clwlkclwwlk  29982  3pthdlem1  30144  frgrregord013  30375  grpoidinvlem3  30486  nmoubi  30752  lnon0  30778  adjsym  31813  nmopub  31888  nmfnleub  31905  cvbr2  32263  chpssati  32343  chrelat2i  32345  chrelat3  32351  mdsymlem8  32390  ralcom4f  32446  reuxfrdf  32470  n0nsnel  32495  uniinn0  32530  ssiun3  32538  disjnf  32550  disjorf  32559  disjunsn  32574  ac6sf2  32605  nn0min  32803  tosglblem  32955  archiabl  33167  1arithidom  33502  eulerpartlems  34373  eulerpartlemr  34387  eulerpartlemn  34394  ballotlem7  34549  bnj110  34870  bnj92  34874  bnj539  34903  bnj540  34904  bnj580  34925  bnj978  34961  bnj1047  34985  bnj1128  35002  bnj1417  35053  bnj1421  35054  bnj1312  35070  bnj1498  35073  onvf1od  35151  lfuhgr3  35164  subfacp1lem3  35226  cvmlift2lem1  35346  cvmlift2lem12  35358  satfv1  35407  fmlaomn0  35434  fmla0disjsuc  35442  fmlasucdisj  35443  untuni  35753  dfso3  35764  elintfv  35809  elpotr  35823  dfon2lem7  35831  dfon2lem9  35833  dfint3  35996  brlb  35999  filnetlem4  36425  bj-reabeq  37071  ctbssinf  37450  fvineqsneq  37456  pibt2  37461  phpreu  37654  ptrecube  37670  poimirlem1  37671  poimirlem25  37695  poimirlem26  37696  poimirlem27  37697  poimirlem30  37700  mblfinlem2  37708  ftc1anc  37751  inixp  37778  ac6gf  37782  heibor1lem  37859  heiborlem1  37861  iscrngo2  38047  ac6s3f  38221  ref5  38361  idinxpssinxp2  38366  n0elqs  38374  ineleq  38396  ssdmral  38413  refrelcosslem  38574  refrelcoss3  38575  lpssat  39122  lssat  39125  lcvbr2  39131  lcvbr3  39132  lfl1  39179  lub0N  39298  glb0N  39302  atlrelat1  39430  hlrelat2  39512  ispsubsp2  39855  pclclN  40000  cdleme25cv  40467  tendoeq2  40883  cdlemk35  41021  aks4d1p7  42186  sticksstones1  42249  indstrd  42296  supinf  42345  infdesc  42746  setindtrs  43128  unielss  43321  ssunib  43323  onsupmaxb  43342  onsupeqnmax  43350  cllem0  43669  ntrneixb  44198  gneispace  44237  expandral  44393  ismnuprim  44397  dfuniv2  44405  undisjrab  44409  zfregs2VD  44943  sswfaxreg  45090  dfac5prim  45093  permac8prim  45117  iindif2f  45267  ralfal  45268  disjinfi  45299  iuneqfzuz  45444  caucvgbf  45597  rexanuz2nf  45600  mccl  45708  limsupub  45812  limsuppnflem  45818  limsupre2lem  45832  lmbr3v  45853  liminfpnfuz  45924  xlimpnfxnegmnf2  45966  ioodvbdlimc1lem2  46040  ioodvbdlimc2lem  46042  dvnprodlem3  46056  fourierdlem103  46317  fourierdlem104  46318  sge0iunmpt  46526  meaiuninc3v  46592  hoidmvle  46708  issmff  46842  n0nsn2el  47135  r19.32  47208  2rexrsb  47212  cbvral2  47213  2reu3  47220  2reu8i  47223  otiunsndisjX  47389  0nelsetpreimafv  47500  dfgric2  48025  gpg5nbgrvtx03starlem1  48178  gpg5nbgrvtx03starlem2  48179  gpg5nbgrvtx03starlem3  48180  gpg5nbgrvtx13starlem1  48181  gpg5nbgrvtx13starlem2  48182  gpg5nbgrvtx13starlem3  48183  gpg5edgnedg  48240  copisnmnd  48279  lindslinindsimp1  48568  lindslinindsimp2  48574  snlindsntor  48582  ldepslinc  48620  iuneq0  48929  iinxp  48941  iscnrm3  49062  setrec1lem3  49800  aacllem  49912