Theorem ralbiia 3091

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2106  ∀wral 3061

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 206  df-ral 3062

This theorem is referenced by:  ralbii  3093  ralanid  3095  poinxp  5756  soinxp  5757  seinxp  5759  dffun8  6576  funcnv3  6618  fncnv  6621  fnres  6677  fvreseq0  7039  isoini2  7338  smores  8354  tfr3ALT  8404  resixp  8929  ixpfi2  9352  marypha1lem  9430  ac5num  10033  acni2  10043  acndom  10048  dfac4  10119  brdom7disj  10528  brdom6disj  10529  fpwwe2lem7  10634  axgroth6  10825  rabssnn0fi  13955  lo1res  15507  isprm5  16648  prmreclem2  16854  tsrss  18546  gass  19206  efgval2  19633  efgsres  19647  acsfn1p  20558  isdomn2  21115  islinds2  21587  isclo  22811  ptclsg  23339  ufilcmp  23756  cfilres  25037  ovolgelb  25221  volsup2  25346  vitali  25354  itg1climres  25456  itg2seq  25484  itg2monolem1  25492  itg2mono  25495  itg2i1fseq  25497  itg2cn  25505  ellimc2  25618  rolle  25731  lhop1  25755  itgsubstlem  25789  tdeglem4  25801  tdeglem4OLD  25802  dvdsmulf1o  26922  dchrelbas2  26964  selbergsb  27302  axcontlem2  28478  dfconngr1  29696  hodsi  31283  ho01i  31336  ho02i  31337  lnopeqi  31516  nmcopexi  31535  nmcfnexi  31559  cnlnadjlem3  31577  cnlnadjlem5  31579  leop3  31633  pjssposi  31680  largei  31775  mdsl2i  31830  mdsl2bi  31831  elat2  31848  dmdbr5ati  31930  cdj3lem3b  31948  subfacp1lem3  34459  dfso3  34981  phpreu  36775  ptrecube  36791  mblfinlem1  36828  voliunnfl  36835  disjressuc2  37561  alephiso2  42611  ntrneiel2  43139  ismbl3  45001  ismbl4  45008  sge0lefimpt  45438  sbgoldbalt  46748