Theorem ralbiia 3108

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 274	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3106	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2142  ∀wral 3078

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838

This proof depends on definitions:  df-bi 210  df-ral 3079

This theorem is used by:  ralbii  3110  ralanid  3112  poinxp  5741  soinxp  5742  seinxp  5744  dffun8  6564  funcnv3  6606  fncnv  6609  fnres  6662  fvreseq0  7033  isoini2  7337  smores  8337  tfr3ALT  8387  resixp  8929  ixpfi2  9305  marypha1lem  9391  ac5num  10027  acni2  10037  acndom  10042  dfac4  10113  brdom7disj  10521  brdom6disj  10522  fpwwe2lem7  10628  axgroth6  10819  rabssnn0fi  14029  lo1res  15617  isprm5  16772  prmreclem2  16983  tsrss  18651  gass  19377  efgval2  19800  efgsres  19814  isdomn2  20821  acsfn1p  20913  islinds2  21974  isclo  23255  ptclsg  23783  ufilcmp  24200  cfilres  25466  ovolgelb  25650  volsup2  25775  vitali  25783  itg1climres  25884  itg2seq  25912  itg2monolem1  25920  itg2mono  25923  itg2i1fseq  25925  itg2cn  25933  ellimc2  26047  rolle  26160  lhop1  26184  itgsubstlem  26218  tdeglem4  26228  mpodvdsmulf1o  27369  dvdsmulf1o  27371  dchrelbas2  27412  selbergsb  27750  axcontlem2  29326  dfconngr1  30550  hodsi  32138  ho01i  32191  ho02i  32192  lnopeqi  32371  nmcopexi  32390  nmcfnexi  32414  cnlnadjlem3  32432  cnlnadjlem5  32434  leop3  32488  pjssposi  32535  largei  32630  mdsl2i  32685  mdsl2bi  32686  elat2  32703  dmdbr5ati  32785  cdj3lem3b  32803  subfacp1lem3  35682  dfso3  36220  phpreu  38283  ptrecube  38299  mblfinlem1  38336  voliunnfl  38343  ralrnmo  39038  raldmqsmo  39040  disjressuc2  39088  fimgmcyc  43330  alephiso2  44312  ntrneiel2  44840  wfac8prim  45739  ismbl3  46728  ismbl4  46735  sge0lefimpt  47165  sbgoldbalt  48574