Theorem ralbiia 3076

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2111  ∀wral 3047

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

This theorem depends on definitions:  df-bi 207  df-ral 3048

This theorem is referenced by:  ralbii  3078  ralanid  3080  poinxp  5695  soinxp  5696  seinxp  5698  dffun8  6509  funcnv3  6551  fncnv  6554  fnres  6608  fvreseq0  6971  isoini2  7273  smores  8272  tfr3ALT  8321  resixp  8857  ixpfi2  9234  marypha1lem  9317  ac5num  9927  acni2  9937  acndom  9942  dfac4  10013  brdom7disj  10422  brdom6disj  10423  fpwwe2lem7  10528  axgroth6  10719  rabssnn0fi  13893  lo1res  15466  isprm5  16618  prmreclem2  16829  tsrss  18495  gass  19213  efgval2  19636  efgsres  19650  isdomn2  20626  isdomn2OLD  20627  acsfn1p  20714  islinds2  21750  isclo  23002  ptclsg  23530  ufilcmp  23947  cfilres  25223  ovolgelb  25408  volsup2  25533  vitali  25541  itg1climres  25642  itg2seq  25670  itg2monolem1  25678  itg2mono  25681  itg2i1fseq  25683  itg2cn  25691  ellimc2  25805  rolle  25921  lhop1  25946  itgsubstlem  25982  tdeglem4  25992  mpodvdsmulf1o  27131  dvdsmulf1o  27133  dchrelbas2  27175  selbergsb  27513  axcontlem2  28943  dfconngr1  30168  hodsi  31755  ho01i  31808  ho02i  31809  lnopeqi  31988  nmcopexi  32007  nmcfnexi  32031  cnlnadjlem3  32049  cnlnadjlem5  32051  leop3  32105  pjssposi  32152  largei  32247  mdsl2i  32302  mdsl2bi  32303  elat2  32320  dmdbr5ati  32402  cdj3lem3b  32420  subfacp1lem3  35226  dfso3  35764  phpreu  37643  ptrecube  37659  mblfinlem1  37696  voliunnfl  37703  disjressuc2  38434  fimgmcyc  42626  alephiso2  43650  ntrneiel2  44178  wfac8prim  45094  ismbl3  46083  ismbl4  46090  sge0lefimpt  46520  sbgoldbalt  47880