Theorem ralbii 3090

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

Syntax hints:   ↔ wb 205   ∈ wcel 2108  ∀wral 3063

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

This theorem depends on definitions:  df-bi 206  df-ral 3068

This theorem is referenced by:  2ralbii  3091  r19.26-2  3095  r19.26-3  3096  ralbiim  3098  2ralbiim  3099  dfral2  3164  rexbiOLD  3170  ralnex2  3188  ralinexa  3190  rexanali  3191  nrexralim  3192  nelb  3194  nelbOLD  3195  r19.23v  3207  r19.32v  3267  ralcom13  3284  ralrot3  3286  2ralor  3294  moel  3349  cbvral2vw  3385  cbvral3vw  3387  cbvral2v  3388  cbvral3v  3390  sbralie  3395  ceqsralv  3459  ralxpxfr2d  3568  reu8  3663  2reuswap  3676  2reu5lem2  3686  2rmoswap  3691  rmoanim  3823  rmoanimALT  3824  dfss5  4195  n0el  4292  ralnralall  4446  2reu4lem  4453  r19.12sn  4653  raldifsnb  4726  eqsn  4759  n0snor2el  4761  uni0b  4864  uni0c  4865  ssint  4892  iuniin  4933  iuneq2  4940  iunssf  4970  iunss  4971  ssiinf  4980  iinab  4993  iinun2  4998  iindif1  5000  iindif2  5002  iinin2  5003  iinuni  5023  sspwuni  5025  iinpw  5031  disjor  5050  disjxun  5068  dftr3  5191  reusv3  5323  otiunsndisj  5428  ssrel2  5685  reliun  5715  xpiindi  5733  rexiunxp  5738  ralxpf  5744  rexxpf  5745  dfse2  5997  idrefALT  6007  asymref2  6011  rninxp  6071  dminxp  6072  cnviin  6178  cnvpo  6179  dfpo2  6188  frpoins2fg  6232  wfis2fgOLD  6245  dffun9  6447  funcnv3  6488  fncnv  6491  fnres  6543  mptfnf  6552  fnopabg  6554  mptfng  6556  fint  6637  funimass4  6816  fndmdifeq0  6903  funconstss  6915  f1ompt  6967  idref  7000  fconstfv  7070  dff13f  7110  dff14b  7125  weniso  7205  foov  7424  dfwe2  7602  tfis2f  7677  tfindes  7684  frxp  7938  dfwrecsOLD  8100  tz7.48lem  8242  tz7.49  8246  oeordi  8380  ixpeq2  8657  ixpin  8669  ixpiin  8670  boxriin  8686  findcard3  8987  fimax2g  8990  fissuni  9054  indexfi  9057  dfsup2  9133  sup0riota  9154  infcllem  9176  wemapsolem  9239  zfinf2  9330  oemapso  9370  zfregs2  9422  frins2f  9442  r1elss  9495  rankc1  9559  cp  9580  bnd2  9582  aceq1  9804  aceq2  9806  kmlem7  9843  kmlem12  9848  kmlem13  9849  kmlem15  9851  fin12  10100  ac6num  10166  ac6s2  10173  ac6sf  10176  ac6s4  10177  zorn2lem4  10186  zorn2lem6  10188  zorn2lem7  10189  zorng  10191  ttukeylem6  10201  brdom7disj  10218  brdom6disj  10219  fpwwe2  10330  fpwwe  10333  axgroth5  10511  axgroth4  10519  grothprim  10521  nqereu  10616  dfinfre  11886  infrenegsup  11888  xrsupsslem  12970  xrinfmsslem  12971  xrinfmss2  12974  fzshftral  13273  fsuppmapnn0ub  13643  mptnn0fsuppr  13647  hashgt12el  14065  hashgt12el2  14066  hashbc  14093  s3iunsndisj  14607  cotr2g  14615  rexfiuz  14987  clim0  15143  rpnnen2lem12  15862  gcdcllem1  16134  absproddvds  16250  coprmproddvdslem  16295  vdwmc2  16608  vdwlem13  16622  vdwnn  16627  xpscf  17193  mreacs  17284  acsfn  17285  acsfn1  17287  acsfn2  17289  dfinito2  17634  dftermo2  17635  ispos2  17948  lublecllem  17993  odulub  18040  oduglb  18042  posglbdg  18048  isnmnd  18304  gsumwspan  18400  smndex2dnrinv  18469  isnsg2  18699  oppgid  18878  oppgcntz  18886  efgval2  19245  iscyggen2  19396  iscyg3  19401  oppr1  19791  isnirred  19857  lssne0  20127  isdomn2  20483  iunocv  20798  islindf4  20955  pmatcollpw2lem  21834  isbasis2g  22006  basdif0  22011  tgval2  22014  ntreq0  22136  isclo2  22147  opnnei  22179  neiptopnei  22191  lmres  22359  ist1-3  22408  cmpcov2  22449  cmpsub  22459  is1stc2  22501  1stccn  22522  kgencn  22615  eltx  22627  txkgen  22711  fbun  22899  trfbas  22903  fbunfip  22928  trfil2  22946  isufil2  22967  fixufil  22981  hausflim  23040  txflf  23065  fclsopn  23073  alexsubALTlem3  23108  isclmp  24166  iscau3  24347  iscau4  24348  caucfil  24352  bcth3  24400  ovolgelb  24549  dyadmax  24667  itg2leub  24804  itg2cn  24833  plydivex  25362  vieta1  25377  lgseisenlem2  26429  pnt3  26665  tglowdim2ln  26916  axcontlem12  27246  elntg2  27256  numedglnl  27417  vtxd0nedgb  27758  wlkvtxedg  27913  pthd  28038  2pthdlem1  28196  clwlkclwwlk  28267  3pthdlem1  28429  frgrregord013  28660  grpoidinvlem3  28769  nmoubi  29035  lnon0  29061  adjsym  30096  nmopub  30171  nmfnleub  30188  cvbr2  30546  chpssati  30626  chrelat2i  30628  chrelat3  30634  mdsymlem8  30673  nelbOLDOLD  30718  ralcom4f  30719  reuxfrdf  30740  uniinn0  30791  ssiun3  30799  disjnf  30810  disjorf  30819  disjunsn  30834  ac6sf2  30861  nn0min  31036  tosglblem  31154  archiabl  31354  eulerpartlems  32227  eulerpartlemr  32241  eulerpartlemn  32248  ballotlem7  32402  bnj110  32738  bnj92  32742  bnj539  32771  bnj540  32772  bnj580  32793  bnj978  32829  bnj1047  32853  bnj1128  32870  bnj1417  32921  bnj1421  32922  bnj1312  32938  bnj1498  32941  lfuhgr3  32981  subfacp1lem3  33044  cvmlift2lem1  33164  cvmlift2lem12  33176  satfv1  33225  fmlaomn0  33252  fmla0disjsuc  33260  fmlasucdisj  33261  untuni  33550  dfso3  33566  fnssintima  33578  dfse3  33580  ralxp3f  33588  elintfv  33644  setinds  33660  setinds2f  33661  elpotr  33663  dfon2lem7  33671  dfon2lem9  33673  ttrclresv  33703  frpoins3xpg  33714  frpoins3xp3g  33715  xpord2ind  33721  xpord3ind  33727  soseq  33730  naddcllem  33758  nosepon  33795  nomaxmo  33828  nosupbnd1lem4  33841  conway  33920  eqscut2  33927  etasslt  33934  slerec  33940  bday1s  33952  madebdaylemlrcut  34006  dfint3  34181  brlb  34184  filnetlem4  34497  bj-reabeq  35144  ctbssinf  35504  fvineqsneq  35510  pibt2  35515  phpreu  35688  ptrecube  35704  poimirlem1  35705  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem30  35734  mblfinlem2  35742  ftc1anc  35785  inixp  35813  ac6gf  35817  heibor1lem  35894  heiborlem1  35896  iscrngo2  36082  ac6s3f  36256  3ralbii  36315  idinxpssinxp2  36380  n0elqs  36388  ineleq  36413  refrelcosslem  36507  refrelcoss3  36508  lpssat  36954  lssat  36957  lcvbr2  36963  lcvbr3  36964  lfl1  37011  lub0N  37130  glb0N  37134  atlrelat1  37262  hlrelat2  37344  ispsubsp2  37687  pclclN  37832  cdleme25cv  38299  tendoeq2  38715  cdlemk35  38853  aks4d1p7  40019  sticksstones1  40030  isdomn5  40099  infdesc  40396  setindtrs  40763  cllem0  41062  ss2iundf  41156  ntrneixb  41594  gneispace  41633  expandral  41797  ismnuprim  41801  dfuniv2  41809  undisjrab  41813  zfregs2VD  42350  disjinfi  42620  iuneqfzuz  42764  mccl  43029  limsupub  43135  limsuppnflem  43141  limsupre2lem  43155  lmbr3v  43176  liminfpnfuz  43247  xlimpnfxnegmnf2  43289  ioodvbdlimc1lem2  43363  ioodvbdlimc2lem  43365  dvnprodlem3  43379  fourierdlem103  43640  fourierdlem104  43641  sge0iunmpt  43846  meaiuninc3v  43912  hoidmvle  44028  issmff  44157  r19.32  44477  2rexrsb  44481  cbvral2  44482  2reu3  44489  2reu8i  44492  otiunsndisjX  44658  0nelsetpreimafv  44730  copisnmnd  45251  lindslinindsimp1  45686  lindslinindsimp2  45692  snlindsntor  45700  ldepslinc  45738  iscnrm3  46134  setrec1lem3  46281  aacllem  46391