Theorem ralbii 3076

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

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

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 3046

This theorem is referenced by:  dfral2  3082  ralinexa  3084  rexanali  3085  r19.26-3  3093  ralbiim  3094  2ralbii  3109  3ralbii  3111  4ralbii  3112  2ralbiim  3113  ralnex2  3114  nrexralim  3118  r19.26-2  3119  r19.23v  3162  r19.32v  3171  2ralor  3212  nelb  3214  cbvral2vw  3220  cbvral3vw  3222  ralrot3  3270  ralcom13  3271  ralcom13OLD  3272  sbralieALT  3329  cbvral2v  3344  cbvral3v  3346  ceqsralv  3491  ralxpxfr2d  3615  reu8  3707  2reuswap  3720  2reu5lem2  3730  2rmoswap  3735  rmoanim  3860  rmoanimALT  3861  dfdif3  4083  dfss5  4241  n0el  4330  ralnralall  4481  2reu4lem  4488  r19.12sn  4687  raldifsnb  4763  eqsn  4796  n0snor2el  4800  uni0b  4900  uni0c  4901  ssint  4931  iuniin  4971  iuneq2  4978  iunssf  5011  iunss  5012  ssiinf  5021  iinab  5035  iinun2  5040  iindif1  5042  iindif2  5044  iinin2  5045  iinuni  5065  sspwuni  5067  iinpw  5073  disjor  5092  disjxun  5108  dftr3  5223  reusv3  5363  otiunsndisj  5483  ssrel2  5751  reliun  5782  xpiindi  5802  rexiunxp  5807  ralxpf  5813  rexxpf  5814  dfse2  6074  idrefALT  6087  asymref2  6093  rninxp  6155  dminxp  6156  cnviin  6262  cnvpo  6263  dfpo2  6272  dfse3  6312  frpoins2fg  6320  dffun9  6548  funcnv3  6589  fncnv  6592  fnres  6648  mptfnf  6656  fnopabg  6658  mptfng  6660  fint  6742  funimass4  6928  fndmdifeq0  7019  funconstss  7031  f1ompt  7086  idref  7121  fconstfv  7189  dff13f  7233  dff14b  7249  weniso  7332  fnssintima  7340  foov  7566  imaeqalov  7631  dfwe2  7753  tfis2f  7835  tfindes  7842  frxp  8108  ralxp3f  8119  frpoins3xpg  8122  frpoins3xp3g  8123  xpord2indlem  8129  xpord3inddlem  8136  soseq  8141  tz7.48lem  8412  tz7.49  8416  oeordi  8554  naddcllem  8643  naddunif  8660  naddasslem2  8662  ixpeq2  8887  ixpin  8899  ixpiin  8900  boxriin  8916  findcard3  9236  findcard3OLD  9237  fimax2g  9240  fissuni  9315  indexfi  9318  dfsup2  9402  sup0riota  9424  infcllem  9446  wemapsolem  9510  zfinf2  9602  oemapso  9642  ttrclresv  9677  zfregs2  9693  frins2f  9713  r1elss  9766  rankc1  9830  cp  9851  bnd2  9853  aceq1  10077  aceq2  10079  kmlem7  10117  kmlem12  10122  kmlem13  10123  kmlem15  10125  fin12  10373  ac6num  10439  ac6s2  10446  ac6sf  10449  ac6s4  10450  zorn2lem4  10459  zorn2lem6  10461  zorn2lem7  10462  zorng  10464  ttukeylem6  10474  brdom7disj  10491  brdom6disj  10492  fpwwe2  10603  fpwwe  10606  axgroth5  10784  axgroth4  10792  grothprim  10794  nqereu  10889  dfinfre  12171  infrenegsup  12173  xrsupsslem  13274  xrinfmsslem  13275  xrinfmss2  13278  fzshftral  13583  fsuppmapnn0ub  13967  mptnn0fsuppr  13971  hashgt12el  14394  hashgt12el2  14395  hashbc  14425  s3iunsndisj  14941  cotr2g  14949  rexfiuz  15321  clim0  15479  rpnnen2lem12  16200  gcdcllem1  16476  absproddvds  16594  coprmproddvdslem  16639  vdwmc2  16957  vdwlem13  16971  vdwnn  16976  xpscf  17535  mreacs  17626  acsfn  17627  acsfn1  17629  acsfn2  17631  dfinito2  17972  dftermo2  17973  ispos2  18283  lublecllem  18326  odulub  18373  oduglb  18375  posglbdg  18381  isnmnd  18672  gsumwspan  18780  smndex2dnrinv  18849  isnsg2  19095  oppgid  19295  oppgcntz  19303  efgval2  19661  iscyggen2  19818  iscyg3  19823  oppr1  20266  isnirred  20336  isdomn5  20626  isdomn2OLD  20628  lssne0  20864  iunocv  21597  islindf4  21754  pmatcollpw2lem  22671  isbasis2g  22842  basdif0  22847  tgval2  22850  ntreq0  22971  isclo2  22982  opnnei  23014  neiptopnei  23026  lmres  23194  ist1-3  23243  cmpcov2  23284  cmpsub  23294  is1stc2  23336  1stccn  23357  kgencn  23450  eltx  23462  txkgen  23546  fbun  23734  trfbas  23738  fbunfip  23763  trfil2  23781  isufil2  23802  fixufil  23816  hausflim  23875  txflf  23900  fclsopn  23908  alexsubALTlem3  23943  isclmp  25004  iscau3  25185  iscau4  25186  caucfil  25190  bcth3  25238  ovolgelb  25388  dyadmax  25506  itg2leub  25642  itg2cn  25671  plydivex  26212  vieta1  26227  lgseisenlem2  27294  pnt3  27530  nosepon  27584  nomaxmo  27617  nosupbnd1lem4  27630  conway  27718  eqscut2  27725  etasslt  27732  slerec  27738  bday1s  27750  cuteq1  27753  madebdaylemlrcut  27817  addsproplem4  27886  addsproplem6  27888  addsprop  27890  addsuniflem  27915  mulsuniflem  28059  onscutlt  28172  onsiso  28176  onsfi  28254  bdayn0p1  28265  addhalfcut  28341  tglowdim2ln  28585  axcontlem12  28909  elntg2  28919  numedglnl  29078  vtxd0nedgb  29423  wlkvtxedg  29579  pthd  29706  2pthdlem1  29867  clwlkclwwlk  29938  3pthdlem1  30100  frgrregord013  30331  grpoidinvlem3  30442  nmoubi  30708  lnon0  30734  adjsym  31769  nmopub  31844  nmfnleub  31861  cvbr2  32219  chpssati  32299  chrelat2i  32301  chrelat3  32307  mdsymlem8  32346  ralcom4f  32403  reuxfrdf  32427  n0nsnel  32451  uniinn0  32486  ssiun3  32494  disjnf  32506  disjorf  32515  disjunsn  32530  ac6sf2  32555  nn0min  32752  tosglblem  32907  archiabl  33159  1arithidom  33515  eulerpartlems  34358  eulerpartlemr  34372  eulerpartlemn  34379  ballotlem7  34534  bnj110  34855  bnj92  34859  bnj539  34888  bnj540  34889  bnj580  34910  bnj978  34946  bnj1047  34970  bnj1128  34987  bnj1417  35038  bnj1421  35039  bnj1312  35055  bnj1498  35058  onvf1od  35101  lfuhgr3  35114  subfacp1lem3  35176  cvmlift2lem1  35296  cvmlift2lem12  35308  satfv1  35357  fmlaomn0  35384  fmla0disjsuc  35392  fmlasucdisj  35393  untuni  35703  dfso3  35714  elintfv  35759  setinds  35773  setinds2f  35774  elpotr  35776  dfon2lem7  35784  dfon2lem9  35786  dfint3  35947  brlb  35950  filnetlem4  36376  bj-reabeq  37022  ctbssinf  37401  fvineqsneq  37407  pibt2  37412  phpreu  37605  ptrecube  37621  poimirlem1  37622  poimirlem25  37646  poimirlem26  37647  poimirlem27  37648  poimirlem30  37651  mblfinlem2  37659  ftc1anc  37702  inixp  37729  ac6gf  37733  heibor1lem  37810  heiborlem1  37812  iscrngo2  37998  ac6s3f  38172  ref5  38308  idinxpssinxp2  38313  n0elqs  38321  ineleq  38343  refrelcosslem  38460  refrelcoss3  38461  lpssat  39013  lssat  39016  lcvbr2  39022  lcvbr3  39023  lfl1  39070  lub0N  39189  glb0N  39193  atlrelat1  39321  hlrelat2  39404  ispsubsp2  39747  pclclN  39892  cdleme25cv  40359  tendoeq2  40775  cdlemk35  40913  aks4d1p7  42078  sticksstones1  42141  indstrd  42188  supinf  42237  infdesc  42638  setindtrs  43021  unielss  43214  ssunib  43216  onsupmaxb  43235  onsupeqnmax  43243  cllem0  43562  ntrneixb  44091  gneispace  44130  expandral  44286  ismnuprim  44290  dfuniv2  44298  undisjrab  44302  zfregs2VD  44837  sswfaxreg  44984  dfac5prim  44987  permac8prim  45011  iindif2f  45161  ralfal  45162  disjinfi  45193  iuneqfzuz  45338  caucvgbf  45492  rexanuz2nf  45495  mccl  45603  limsupub  45709  limsuppnflem  45715  limsupre2lem  45729  lmbr3v  45750  liminfpnfuz  45821  xlimpnfxnegmnf2  45863  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem3  45953  fourierdlem103  46214  fourierdlem104  46215  sge0iunmpt  46423  meaiuninc3v  46489  hoidmvle  46605  issmff  46739  n0nsn2el  47030  r19.32  47103  2rexrsb  47107  cbvral2  47108  2reu3  47115  2reu8i  47118  otiunsndisjX  47284  0nelsetpreimafv  47395  dfgric2  47919  gpg5nbgrvtx03starlem1  48063  gpg5nbgrvtx03starlem2  48064  gpg5nbgrvtx03starlem3  48065  gpg5nbgrvtx13starlem1  48066  gpg5nbgrvtx13starlem2  48067  gpg5nbgrvtx13starlem3  48068  copisnmnd  48161  lindslinindsimp1  48450  lindslinindsimp2  48456  snlindsntor  48464  ldepslinc  48502  iuneq0  48811  iinxp  48823  iscnrm3  48944  setrec1lem3  49682  aacllem  49794