Theorem ralbiia 3080

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2114  ∀wral 3054

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

This theorem depends on definitions:  df-bi 210  df-ral 3059

This theorem is referenced by:  ralbii  3081  ralanid  3084  poinxp  5613  soinxp  5614  seinxp  5616  dffun8  6377  funcnv3  6419  fncnv  6422  fnres  6473  fvreseq0  6827  isoini2  7117  smores  8030  tfr3ALT  8079  resixp  8555  ixpfi2  8907  marypha1lem  8982  ac5num  9548  acni2  9558  acndom  9563  dfac4  9634  brdom7disj  10043  brdom6disj  10044  fpwwe2lem7  10149  axgroth6  10340  rabssnn0fi  13457  lo1res  15018  isprm5  16160  prmreclem2  16365  tsrss  17961  gass  18561  efgval2  18980  efgsres  18994  acsfn1p  19709  isdomn2  20203  islinds2  20641  isclo  21850  ptclsg  22378  ufilcmp  22795  cfilres  24060  ovolgelb  24244  volsup2  24369  vitali  24377  itg1climres  24479  itg2seq  24507  itg2monolem1  24515  itg2mono  24518  itg2i1fseq  24520  itg2cn  24528  ellimc2  24641  rolle  24754  lhop1  24778  itgsubstlem  24812  tdeglem4  24824  tdeglem4OLD  24825  dvdsmulf1o  25943  dchrelbas2  25985  selbergsb  26323  axcontlem2  26923  dfconngr1  28137  hodsi  29722  ho01i  29775  ho02i  29776  lnopeqi  29955  nmcopexi  29974  nmcfnexi  29998  cnlnadjlem3  30016  cnlnadjlem5  30018  leop3  30072  pjssposi  30119  largei  30214  mdsl2i  30269  mdsl2bi  30270  elat2  30287  dmdbr5ati  30369  cdj3lem3b  30387  subfacp1lem3  32727  dfso3  33249  phpreu  35416  ptrecube  35432  mblfinlem1  35469  voliunnfl  35476  alephiso2  40750  ntrneiel2  41282  ismbl3  43109  ismbl4  43116  sge0lefimpt  43543  sbgoldbalt  44814