Theorem ralbiia 3092

Description: Inference adding restricted universal quantifier to both sides of an equivalence. (Contributed by NM, 26-Nov-2000.)

Hypothesis

Ref	Expression
ralbiia.1	⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))

Assertion

Ref	Expression
ralbiia	⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Proof of Theorem ralbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓))
2	1	pm5.74i 271	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3090	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∀wral 3062

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

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

This theorem is referenced by:  ralbii  3094  ralanid  3096  poinxp  5757  soinxp  5758  seinxp  5760  dffun8  6577  funcnv3  6619  fncnv  6622  fnres  6678  fvreseq0  7040  isoini2  7336  smores  8352  tfr3ALT  8402  resixp  8927  ixpfi2  9350  marypha1lem  9428  ac5num  10031  acni2  10041  acndom  10046  dfac4  10117  brdom7disj  10526  brdom6disj  10527  fpwwe2lem7  10632  axgroth6  10823  rabssnn0fi  13951  lo1res  15503  isprm5  16644  prmreclem2  16850  tsrss  18542  gass  19165  efgval2  19592  efgsres  19606  acsfn1p  20415  isdomn2  20915  islinds2  21368  isclo  22591  ptclsg  23119  ufilcmp  23536  cfilres  24813  ovolgelb  24997  volsup2  25122  vitali  25130  itg1climres  25232  itg2seq  25260  itg2monolem1  25268  itg2mono  25271  itg2i1fseq  25273  itg2cn  25281  ellimc2  25394  rolle  25507  lhop1  25531  itgsubstlem  25565  tdeglem4  25577  tdeglem4OLD  25578  dvdsmulf1o  26698  dchrelbas2  26740  selbergsb  27078  axcontlem2  28223  dfconngr1  29441  hodsi  31028  ho01i  31081  ho02i  31082  lnopeqi  31261  nmcopexi  31280  nmcfnexi  31304  cnlnadjlem3  31322  cnlnadjlem5  31324  leop3  31378  pjssposi  31425  largei  31520  mdsl2i  31575  mdsl2bi  31576  elat2  31593  dmdbr5ati  31675  cdj3lem3b  31693  subfacp1lem3  34173  dfso3  34689  phpreu  36472  ptrecube  36488  mblfinlem1  36525  voliunnfl  36532  disjressuc2  37258  alephiso2  42309  ntrneiel2  42837  ismbl3  44702  ismbl4  44709  sge0lefimpt  45139  sbgoldbalt  46449