Theorem ralbiia 3082

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3052

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

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

This theorem is referenced by:  ralbii  3084  ralanid  3086  poinxp  5707  soinxp  5708  seinxp  5710  dffun8  6522  funcnv3  6564  fncnv  6567  fnres  6621  fvreseq0  6986  isoini2  7289  smores  8287  tfr3ALT  8336  resixp  8876  ixpfi2  9255  marypha1lem  9341  ac5num  9953  acni2  9963  acndom  9968  dfac4  10039  brdom7disj  10448  brdom6disj  10449  fpwwe2lem7  10555  axgroth6  10746  rabssnn0fi  13943  lo1res  15516  isprm5  16672  prmreclem2  16883  tsrss  18550  gass  19271  efgval2  19694  efgsres  19708  isdomn2  20683  isdomn2OLD  20684  acsfn1p  20771  islinds2  21807  isclo  23066  ptclsg  23594  ufilcmp  24011  cfilres  25277  ovolgelb  25461  volsup2  25586  vitali  25594  itg1climres  25695  itg2seq  25723  itg2monolem1  25731  itg2mono  25734  itg2i1fseq  25736  itg2cn  25744  ellimc2  25858  rolle  25971  lhop1  25995  itgsubstlem  26029  tdeglem4  26039  mpodvdsmulf1o  27175  dvdsmulf1o  27177  dchrelbas2  27218  selbergsb  27556  axcontlem2  29052  dfconngr1  30277  hodsi  31865  ho01i  31918  ho02i  31919  lnopeqi  32098  nmcopexi  32117  nmcfnexi  32141  cnlnadjlem3  32159  cnlnadjlem5  32161  leop3  32215  pjssposi  32262  largei  32357  mdsl2i  32412  mdsl2bi  32413  elat2  32430  dmdbr5ati  32512  cdj3lem3b  32530  subfacp1lem3  35384  dfso3  35922  phpreu  37943  ptrecube  37959  mblfinlem1  37996  voliunnfl  38003  ralrnmo  38700  raldmqsmo  38702  disjressuc2  38750  fimgmcyc  42997  alephiso2  44007  ntrneiel2  44535  wfac8prim  45451  ismbl3  46436  ismbl4  46443  sge0lefimpt  46873  sbgoldbalt  48273