Theorem ralbiia 3089

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2106  ∀wral 3059

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

This theorem depends on definitions:  df-bi 207  df-ral 3060

This theorem is referenced by:  ralbii  3091  ralanid  3093  poinxp  5769  soinxp  5770  seinxp  5772  dffun8  6596  funcnv3  6638  fncnv  6641  fnres  6696  fvreseq0  7058  isoini2  7359  smores  8391  tfr3ALT  8441  resixp  8972  ixpfi2  9388  marypha1lem  9471  ac5num  10074  acni2  10084  acndom  10089  dfac4  10160  brdom7disj  10569  brdom6disj  10570  fpwwe2lem7  10675  axgroth6  10866  rabssnn0fi  14024  lo1res  15592  isprm5  16741  prmreclem2  16951  tsrss  18647  gass  19332  efgval2  19757  efgsres  19771  isdomn2  20728  isdomn2OLD  20729  acsfn1p  20817  islinds2  21851  isclo  23111  ptclsg  23639  ufilcmp  24056  cfilres  25344  ovolgelb  25529  volsup2  25654  vitali  25662  itg1climres  25764  itg2seq  25792  itg2monolem1  25800  itg2mono  25803  itg2i1fseq  25805  itg2cn  25813  ellimc2  25927  rolle  26043  lhop1  26068  itgsubstlem  26104  tdeglem4  26114  mpodvdsmulf1o  27252  dvdsmulf1o  27254  dchrelbas2  27296  selbergsb  27634  axcontlem2  28995  dfconngr1  30217  hodsi  31804  ho01i  31857  ho02i  31858  lnopeqi  32037  nmcopexi  32056  nmcfnexi  32080  cnlnadjlem3  32098  cnlnadjlem5  32100  leop3  32154  pjssposi  32201  largei  32296  mdsl2i  32351  mdsl2bi  32352  elat2  32369  dmdbr5ati  32451  cdj3lem3b  32469  subfacp1lem3  35167  dfso3  35700  phpreu  37591  ptrecube  37607  mblfinlem1  37644  voliunnfl  37651  disjressuc2  38370  fimgmcyc  42521  alephiso2  43548  ntrneiel2  44076  ismbl3  45942  ismbl4  45949  sge0lefimpt  46379  sbgoldbalt  47706