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  3080  ralinexa  3082  rexanali  3083  r19.26-3  3090  ralbiim  3091  2ralbii  3104  3ralbii  3106  4ralbii  3107  2ralbiim  3108  ralnex2  3109  nrexralim  3113  r19.26-2  3114  r19.23v  3156  r19.32v  3162  2ralor  3203  nelb  3205  cbvral2vw  3211  cbvral3vw  3213  ralrot3  3260  ralcom13  3261  sbralieALT  3316  cbvral2v  3331  cbvral3v  3333  ceqsralv  3474  ralxpxfr2d  3598  reu8  3689  2reuswap  3702  2reu5lem2  3712  2rmoswap  3717  rmoanim  3842  rmoanimALT  3843  dfdif3  4064  dfss5  4222  n0el  4311  ralnralall  4462  2reu4lem  4469  r19.12sn  4670  raldifsnb  4745  eqsn  4778  n0snor2el  4782  uni0b  4882  uni0c  4883  ssint  4911  iuniin  4951  iuneq2  4958  iunssf  4990  iunss  4991  ssiinf  5000  iinab  5013  iinun2  5018  iindif1  5020  iindif2  5022  iinin2  5023  iinuni  5043  sspwuni  5045  iinpw  5051  disjor  5070  disjxun  5086  dftr3  5200  reusv3  5340  otiunsndisj  5457  ssrel2  5722  reliun  5753  xpiindi  5772  rexiunxp  5777  ralxpf  5783  rexxpf  5784  dfse2  6045  idrefALT  6056  asymref2  6060  rninxp  6122  dminxp  6123  cnviin  6228  cnvpo  6229  dfpo2  6238  dfse3  6278  frpoins2fg  6286  dffun9  6505  funcnv3  6546  fncnv  6549  fnres  6603  mptfnf  6611  fnopabg  6613  mptfng  6615  fint  6697  funimass4  6880  fndmdifeq0  6971  funconstss  6983  f1ompt  7038  idref  7073  fconstfv  7140  dff13f  7183  dff14b  7199  weniso  7282  fnssintima  7290  foov  7514  imaeqalov  7579  dfwe2  7701  tfis2f  7780  tfindes  7787  frxp  8050  ralxp3f  8061  frpoins3xpg  8064  frpoins3xp3g  8065  xpord2indlem  8071  xpord3inddlem  8078  soseq  8083  tz7.48lem  8354  tz7.49  8358  oeordi  8496  naddcllem  8585  naddunif  8602  naddasslem2  8604  ixpeq2  8829  ixpin  8841  ixpiin  8842  boxriin  8858  findcard3  9161  fimax2g  9164  fissuni  9235  indexfi  9238  dfsup2  9322  sup0riota  9344  infcllem  9366  wemapsolem  9430  zfinf2  9526  oemapso  9566  ttrclresv  9601  zfregs2  9617  frins2f  9637  r1elss  9690  rankc1  9754  cp  9775  bnd2  9777  aceq1  9999  aceq2  10001  kmlem7  10039  kmlem12  10044  kmlem13  10045  kmlem15  10047  fin12  10295  ac6num  10361  ac6s2  10368  ac6sf  10371  ac6s4  10372  zorn2lem4  10381  zorn2lem6  10383  zorn2lem7  10384  zorng  10386  ttukeylem6  10396  brdom7disj  10413  brdom6disj  10414  fpwwe2  10525  fpwwe  10528  axgroth5  10706  axgroth4  10714  grothprim  10716  nqereu  10811  dfinfre  12094  infrenegsup  12096  xrsupsslem  13197  xrinfmsslem  13198  xrinfmss2  13201  fzshftral  13506  fsuppmapnn0ub  13890  mptnn0fsuppr  13894  hashgt12el  14317  hashgt12el2  14318  hashbc  14348  s3iunsndisj  14862  cotr2g  14870  rexfiuz  15242  clim0  15400  rpnnen2lem12  16121  gcdcllem1  16397  absproddvds  16515  coprmproddvdslem  16560  vdwmc2  16878  vdwlem13  16892  vdwnn  16897  xpscf  17456  mreacs  17551  acsfn  17552  acsfn1  17554  acsfn2  17556  dfinito2  17897  dftermo2  17898  ispos2  18208  lublecllem  18251  odulub  18298  oduglb  18300  posglbdg  18306  isnmnd  18599  gsumwspan  18707  smndex2dnrinv  18776  isnsg2  19022  oppgid  19222  oppgcntz  19230  efgval2  19590  iscyggen2  19747  iscyg3  19752  oppr1  20222  isnirred  20292  isdomn5  20579  isdomn2OLD  20581  lssne0  20838  iunocv  21572  islindf4  21729  pmatcollpw2lem  22646  isbasis2g  22817  basdif0  22822  tgval2  22825  ntreq0  22946  isclo2  22957  opnnei  22989  neiptopnei  23001  lmres  23169  ist1-3  23218  cmpcov2  23259  cmpsub  23269  is1stc2  23311  1stccn  23332  kgencn  23425  eltx  23437  txkgen  23521  fbun  23709  trfbas  23713  fbunfip  23738  trfil2  23756  isufil2  23777  fixufil  23791  hausflim  23850  txflf  23875  fclsopn  23883  alexsubALTlem3  23918  isclmp  24978  iscau3  25159  iscau4  25160  caucfil  25164  bcth3  25212  ovolgelb  25362  dyadmax  25480  itg2leub  25616  itg2cn  25645  plydivex  26186  vieta1  26201  lgseisenlem2  27268  pnt3  27504  nosepon  27558  nomaxmo  27591  nosupbnd1lem4  27604  conway  27694  eqscut2  27701  etasslt  27708  slerec  27714  bday1s  27729  cuteq1  27732  madebdaylemlrcut  27798  addsproplem4  27869  addsproplem6  27871  addsprop  27873  addsuniflem  27898  mulsuniflem  28042  onscutlt  28155  onsiso  28159  onsfi  28237  bdayn0p1  28248  addhalfcut  28333  tglowdim2ln  28583  axcontlem12  28907  elntg2  28917  numedglnl  29076  vtxd0nedgb  29421  wlkvtxedg  29576  pthd  29701  2pthdlem1  29862  clwlkclwwlk  29933  3pthdlem1  30095  frgrregord013  30326  grpoidinvlem3  30437  nmoubi  30703  lnon0  30729  adjsym  31764  nmopub  31839  nmfnleub  31856  cvbr2  32214  chpssati  32294  chrelat2i  32296  chrelat3  32302  mdsymlem8  32341  ralcom4f  32398  reuxfrdf  32422  n0nsnel  32447  uniinn0  32482  ssiun3  32490  disjnf  32502  disjorf  32511  disjunsn  32526  ac6sf2  32557  nn0min  32758  tosglblem  32911  archiabl  33135  1arithidom  33470  eulerpartlems  34341  eulerpartlemr  34355  eulerpartlemn  34362  ballotlem7  34517  bnj110  34838  bnj92  34842  bnj539  34871  bnj540  34872  bnj580  34893  bnj978  34929  bnj1047  34953  bnj1128  34970  bnj1417  35021  bnj1421  35022  bnj1312  35038  bnj1498  35041  onvf1od  35097  lfuhgr3  35110  subfacp1lem3  35172  cvmlift2lem1  35292  cvmlift2lem12  35304  satfv1  35353  fmlaomn0  35380  fmla0disjsuc  35388  fmlasucdisj  35389  untuni  35699  dfso3  35710  elintfv  35755  setinds  35769  setinds2f  35770  elpotr  35772  dfon2lem7  35780  dfon2lem9  35782  dfint3  35943  brlb  35946  filnetlem4  36372  bj-reabeq  37018  ctbssinf  37397  fvineqsneq  37403  pibt2  37408  phpreu  37601  ptrecube  37617  poimirlem1  37618  poimirlem25  37642  poimirlem26  37643  poimirlem27  37644  poimirlem30  37647  mblfinlem2  37655  ftc1anc  37698  inixp  37725  ac6gf  37729  heibor1lem  37806  heiborlem1  37808  iscrngo2  37994  ac6s3f  38168  ref5  38304  idinxpssinxp2  38309  n0elqs  38317  ineleq  38339  refrelcosslem  38456  refrelcoss3  38457  lpssat  39009  lssat  39012  lcvbr2  39018  lcvbr3  39019  lfl1  39066  lub0N  39185  glb0N  39189  atlrelat1  39317  hlrelat2  39399  ispsubsp2  39742  pclclN  39887  cdleme25cv  40354  tendoeq2  40770  cdlemk35  40908  aks4d1p7  42073  sticksstones1  42136  indstrd  42183  supinf  42232  infdesc  42633  setindtrs  43015  unielss  43208  ssunib  43210  onsupmaxb  43229  onsupeqnmax  43237  cllem0  43556  ntrneixb  44085  gneispace  44124  expandral  44280  ismnuprim  44284  dfuniv2  44292  undisjrab  44296  zfregs2VD  44830  sswfaxreg  44977  dfac5prim  44980  permac8prim  45004  iindif2f  45154  ralfal  45155  disjinfi  45186  iuneqfzuz  45331  caucvgbf  45484  rexanuz2nf  45487  mccl  45595  limsupub  45699  limsuppnflem  45705  limsupre2lem  45719  lmbr3v  45740  liminfpnfuz  45811  xlimpnfxnegmnf2  45853  ioodvbdlimc1lem2  45927  ioodvbdlimc2lem  45929  dvnprodlem3  45943  fourierdlem103  46204  fourierdlem104  46205  sge0iunmpt  46413  meaiuninc3v  46479  hoidmvle  46595  issmff  46729  n0nsn2el  47023  r19.32  47096  2rexrsb  47100  cbvral2  47101  2reu3  47108  2reu8i  47111  otiunsndisjX  47277  0nelsetpreimafv  47388  dfgric2  47913  gpg5nbgrvtx03starlem1  48066  gpg5nbgrvtx03starlem2  48067  gpg5nbgrvtx03starlem3  48068  gpg5nbgrvtx13starlem1  48069  gpg5nbgrvtx13starlem2  48070  gpg5nbgrvtx13starlem3  48071  gpg5edgnedg  48128  copisnmnd  48167  lindslinindsimp1  48456  lindslinindsimp2  48462  snlindsntor  48470  ldepslinc  48508  iuneq0  48817  iinxp  48829  iscnrm3  48950  setrec1lem3  49688  aacllem  49800