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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2108  ∀wral 3063

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

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

This theorem is referenced by:  ralbii  3090  ralanid  3093  poinxp  5658  soinxp  5659  seinxp  5661  dffun8  6446  funcnv3  6488  fncnv  6491  fnres  6543  fvreseq0  6897  isoini2  7190  smores  8154  tfr3ALT  8204  resixp  8679  ixpfi2  9047  marypha1lem  9122  ac5num  9723  acni2  9733  acndom  9738  dfac4  9809  brdom7disj  10218  brdom6disj  10219  fpwwe2lem7  10324  axgroth6  10515  rabssnn0fi  13634  lo1res  15196  isprm5  16340  prmreclem2  16546  tsrss  18222  gass  18822  efgval2  19245  efgsres  19259  acsfn1p  19982  isdomn2  20483  islinds2  20930  isclo  22146  ptclsg  22674  ufilcmp  23091  cfilres  24365  ovolgelb  24549  volsup2  24674  vitali  24682  itg1climres  24784  itg2seq  24812  itg2monolem1  24820  itg2mono  24823  itg2i1fseq  24825  itg2cn  24833  ellimc2  24946  rolle  25059  lhop1  25083  itgsubstlem  25117  tdeglem4  25129  tdeglem4OLD  25130  dvdsmulf1o  26248  dchrelbas2  26290  selbergsb  26628  axcontlem2  27236  dfconngr1  28453  hodsi  30038  ho01i  30091  ho02i  30092  lnopeqi  30271  nmcopexi  30290  nmcfnexi  30314  cnlnadjlem3  30332  cnlnadjlem5  30334  leop3  30388  pjssposi  30435  largei  30530  mdsl2i  30585  mdsl2bi  30586  elat2  30603  dmdbr5ati  30685  cdj3lem3b  30703  subfacp1lem3  33044  dfso3  33566  phpreu  35688  ptrecube  35704  mblfinlem1  35741  voliunnfl  35748  alephiso2  41054  ntrneiel2  41585  ismbl3  43417  ismbl4  43424  sge0lefimpt  43851  sbgoldbalt  45121