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  3161  r19.32v  3170  2ralor  3211  nelb  3213  cbvral2vw  3219  cbvral3vw  3221  ralrot3  3268  ralcom13  3269  ralcom13OLD  3270  sbralieALT  3327  cbvral2v  3342  cbvral3v  3344  ceqsralv  3488  ralxpxfr2d  3612  reu8  3704  2reuswap  3717  2reu5lem2  3727  2rmoswap  3732  rmoanim  3857  rmoanimALT  3858  dfdif3  4080  dfss5  4238  n0el  4327  ralnralall  4478  2reu4lem  4485  r19.12sn  4684  raldifsnb  4760  eqsn  4793  n0snor2el  4797  uni0b  4897  uni0c  4898  ssint  4928  iuniin  4968  iuneq2  4975  iunssf  5008  iunss  5009  ssiinf  5018  iinab  5032  iinun2  5037  iindif1  5039  iindif2  5041  iinin2  5042  iinuni  5062  sspwuni  5064  iinpw  5070  disjor  5089  disjxun  5105  dftr3  5220  reusv3  5360  otiunsndisj  5480  ssrel2  5748  reliun  5779  xpiindi  5799  rexiunxp  5804  ralxpf  5810  rexxpf  5811  dfse2  6071  idrefALT  6084  asymref2  6090  rninxp  6152  dminxp  6153  cnviin  6259  cnvpo  6260  dfpo2  6269  dfse3  6309  frpoins2fg  6317  dffun9  6545  funcnv3  6586  fncnv  6589  fnres  6645  mptfnf  6653  fnopabg  6655  mptfng  6657  fint  6739  funimass4  6925  fndmdifeq0  7016  funconstss  7028  f1ompt  7083  idref  7118  fconstfv  7186  dff13f  7230  dff14b  7246  weniso  7329  fnssintima  7337  foov  7563  imaeqalov  7628  dfwe2  7750  tfis2f  7832  tfindes  7839  frxp  8105  ralxp3f  8116  frpoins3xpg  8119  frpoins3xp3g  8120  xpord2indlem  8126  xpord3inddlem  8133  soseq  8138  tz7.48lem  8409  tz7.49  8413  oeordi  8551  naddcllem  8640  naddunif  8657  naddasslem2  8659  ixpeq2  8884  ixpin  8896  ixpiin  8897  boxriin  8913  findcard3  9229  findcard3OLD  9230  fimax2g  9233  fissuni  9308  indexfi  9311  dfsup2  9395  sup0riota  9417  infcllem  9439  wemapsolem  9503  zfinf2  9595  oemapso  9635  ttrclresv  9670  zfregs2  9686  frins2f  9706  r1elss  9759  rankc1  9823  cp  9844  bnd2  9846  aceq1  10070  aceq2  10072  kmlem7  10110  kmlem12  10115  kmlem13  10116  kmlem15  10118  fin12  10366  ac6num  10432  ac6s2  10439  ac6sf  10442  ac6s4  10443  zorn2lem4  10452  zorn2lem6  10454  zorn2lem7  10455  zorng  10457  ttukeylem6  10467  brdom7disj  10484  brdom6disj  10485  fpwwe2  10596  fpwwe  10599  axgroth5  10777  axgroth4  10785  grothprim  10787  nqereu  10882  dfinfre  12164  infrenegsup  12166  xrsupsslem  13267  xrinfmsslem  13268  xrinfmss2  13271  fzshftral  13576  fsuppmapnn0ub  13960  mptnn0fsuppr  13964  hashgt12el  14387  hashgt12el2  14388  hashbc  14418  s3iunsndisj  14934  cotr2g  14942  rexfiuz  15314  clim0  15472  rpnnen2lem12  16193  gcdcllem1  16469  absproddvds  16587  coprmproddvdslem  16632  vdwmc2  16950  vdwlem13  16964  vdwnn  16969  xpscf  17528  mreacs  17619  acsfn  17620  acsfn1  17622  acsfn2  17624  dfinito2  17965  dftermo2  17966  ispos2  18276  lublecllem  18319  odulub  18366  oduglb  18368  posglbdg  18374  isnmnd  18665  gsumwspan  18773  smndex2dnrinv  18842  isnsg2  19088  oppgid  19288  oppgcntz  19296  efgval2  19654  iscyggen2  19811  iscyg3  19816  oppr1  20259  isnirred  20329  isdomn5  20619  isdomn2OLD  20621  lssne0  20857  iunocv  21590  islindf4  21747  pmatcollpw2lem  22664  isbasis2g  22835  basdif0  22840  tgval2  22843  ntreq0  22964  isclo2  22975  opnnei  23007  neiptopnei  23019  lmres  23187  ist1-3  23236  cmpcov2  23277  cmpsub  23287  is1stc2  23329  1stccn  23350  kgencn  23443  eltx  23455  txkgen  23539  fbun  23727  trfbas  23731  fbunfip  23756  trfil2  23774  isufil2  23795  fixufil  23809  hausflim  23868  txflf  23893  fclsopn  23901  alexsubALTlem3  23936  isclmp  24997  iscau3  25178  iscau4  25179  caucfil  25183  bcth3  25231  ovolgelb  25381  dyadmax  25499  itg2leub  25635  itg2cn  25664  plydivex  26205  vieta1  26220  lgseisenlem2  27287  pnt3  27523  nosepon  27577  nomaxmo  27610  nosupbnd1lem4  27623  conway  27711  eqscut2  27718  etasslt  27725  slerec  27731  bday1s  27743  cuteq1  27746  madebdaylemlrcut  27810  addsproplem4  27879  addsproplem6  27881  addsprop  27883  addsuniflem  27908  mulsuniflem  28052  onscutlt  28165  onsiso  28169  onsfi  28247  bdayn0p1  28258  addhalfcut  28334  tglowdim2ln  28578  axcontlem12  28902  elntg2  28912  numedglnl  29071  vtxd0nedgb  29416  wlkvtxedg  29572  pthd  29699  2pthdlem1  29860  clwlkclwwlk  29931  3pthdlem1  30093  frgrregord013  30324  grpoidinvlem3  30435  nmoubi  30701  lnon0  30727  adjsym  31762  nmopub  31837  nmfnleub  31854  cvbr2  32212  chpssati  32292  chrelat2i  32294  chrelat3  32300  mdsymlem8  32339  ralcom4f  32396  reuxfrdf  32420  n0nsnel  32444  uniinn0  32479  ssiun3  32487  disjnf  32499  disjorf  32508  disjunsn  32523  ac6sf2  32548  nn0min  32745  tosglblem  32900  archiabl  33152  1arithidom  33508  eulerpartlems  34351  eulerpartlemr  34365  eulerpartlemn  34372  ballotlem7  34527  bnj110  34848  bnj92  34852  bnj539  34881  bnj540  34882  bnj580  34903  bnj978  34939  bnj1047  34963  bnj1128  34980  bnj1417  35031  bnj1421  35032  bnj1312  35048  bnj1498  35051  onvf1od  35094  lfuhgr3  35107  subfacp1lem3  35169  cvmlift2lem1  35289  cvmlift2lem12  35301  satfv1  35350  fmlaomn0  35377  fmla0disjsuc  35385  fmlasucdisj  35386  untuni  35696  dfso3  35707  elintfv  35752  setinds  35766  setinds2f  35767  elpotr  35769  dfon2lem7  35777  dfon2lem9  35779  dfint3  35940  brlb  35943  filnetlem4  36369  bj-reabeq  37015  ctbssinf  37394  fvineqsneq  37400  pibt2  37405  phpreu  37598  ptrecube  37614  poimirlem1  37615  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem30  37644  mblfinlem2  37652  ftc1anc  37695  inixp  37722  ac6gf  37726  heibor1lem  37803  heiborlem1  37805  iscrngo2  37991  ac6s3f  38165  ref5  38301  idinxpssinxp2  38306  n0elqs  38314  ineleq  38336  refrelcosslem  38453  refrelcoss3  38454  lpssat  39006  lssat  39009  lcvbr2  39015  lcvbr3  39016  lfl1  39063  lub0N  39182  glb0N  39186  atlrelat1  39314  hlrelat2  39397  ispsubsp2  39740  pclclN  39885  cdleme25cv  40352  tendoeq2  40768  cdlemk35  40906  aks4d1p7  42071  sticksstones1  42134  indstrd  42181  supinf  42230  infdesc  42631  setindtrs  43014  unielss  43207  ssunib  43209  onsupmaxb  43228  onsupeqnmax  43236  cllem0  43555  ntrneixb  44084  gneispace  44123  expandral  44279  ismnuprim  44283  dfuniv2  44291  undisjrab  44295  zfregs2VD  44830  sswfaxreg  44977  dfac5prim  44980  permac8prim  45004  iindif2f  45154  ralfal  45155  disjinfi  45186  iuneqfzuz  45331  caucvgbf  45485  rexanuz2nf  45488  mccl  45596  limsupub  45702  limsuppnflem  45708  limsupre2lem  45722  lmbr3v  45743  liminfpnfuz  45814  xlimpnfxnegmnf2  45856  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem3  45946  fourierdlem103  46207  fourierdlem104  46208  sge0iunmpt  46416  meaiuninc3v  46482  hoidmvle  46598  issmff  46732  n0nsn2el  47026  r19.32  47099  2rexrsb  47103  cbvral2  47104  2reu3  47111  2reu8i  47114  otiunsndisjX  47280  0nelsetpreimafv  47391  dfgric2  47915  gpg5nbgrvtx03starlem1  48059  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx03starlem3  48061  gpg5nbgrvtx13starlem1  48062  gpg5nbgrvtx13starlem2  48063  gpg5nbgrvtx13starlem3  48064  copisnmnd  48157  lindslinindsimp1  48446  lindslinindsimp2  48452  snlindsntor  48460  ldepslinc  48498  iuneq0  48807  iinxp  48819  iscnrm3  48940  setrec1lem3  49678  aacllem  49790