Theorem ralbiia 3164

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2110  ∀wral 3138

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 209  df-ral 3143

This theorem is referenced by:  ralanid  3168  poinxp  5627  soinxp  5628  seinxp  5630  dffun8  6378  funcnv3  6419  fncnv  6422  fnres  6469  fvreseq0  6803  isoini2  7086  smores  7983  tfr3ALT  8032  resixp  8491  ixpfi2  8816  marypha1lem  8891  ac5num  9456  acni2  9466  acndom  9471  dfac4  9542  brdom7disj  9947  brdom6disj  9948  fpwwe2lem8  10053  axgroth6  10244  rabssnn0fi  13348  lo1res  14910  isprm5  16045  prmreclem2  16247  tsrss  17827  gass  18425  efgval2  18844  efgsres  18858  acsfn1p  19572  isdomn2  20066  islinds2  20951  isclo  21689  ptclsg  22217  ufilcmp  22634  cfilres  23893  ovolgelb  24075  volsup2  24200  vitali  24208  itg1climres  24309  itg2seq  24337  itg2monolem1  24345  itg2mono  24348  itg2i1fseq  24350  itg2cn  24358  ellimc2  24469  rolle  24581  lhop1  24605  itgsubstlem  24639  tdeglem4  24648  dvdsmulf1o  25765  dchrelbas2  25807  selbergsb  26145  axcontlem2  26745  dfconngr1  27961  hodsi  29546  ho01i  29599  ho02i  29600  lnopeqi  29779  nmcopexi  29798  nmcfnexi  29822  cnlnadjlem3  29840  cnlnadjlem5  29842  leop3  29896  pjssposi  29943  largei  30038  mdsl2i  30093  mdsl2bi  30094  elat2  30111  dmdbr5ati  30193  cdj3lem3b  30211  subfacp1lem3  32424  dfso3  32945  phpreu  34870  ptrecube  34886  mblfinlem1  34923  voliunnfl  34930  alephiso2  39910  ntrneiel2  40429  ismbl3  42264  ismbl4  42271  sge0lefimpt  42698  sbgoldbalt  43939