Theorem ralbiia 3081

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3052

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

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

This theorem is referenced by:  ralbii  3083  ralanid  3085  poinxp  5740  soinxp  5741  seinxp  5743  dffun8  6569  funcnv3  6611  fncnv  6614  fnres  6670  fvreseq0  7033  isoini2  7337  smores  8371  tfr3ALT  8421  resixp  8952  ixpfi2  9367  marypha1lem  9450  ac5num  10055  acni2  10065  acndom  10070  dfac4  10141  brdom7disj  10550  brdom6disj  10551  fpwwe2lem7  10656  axgroth6  10847  rabssnn0fi  14009  lo1res  15580  isprm5  16731  prmreclem2  16942  tsrss  18604  gass  19289  efgval2  19710  efgsres  19724  isdomn2  20676  isdomn2OLD  20677  acsfn1p  20764  islinds2  21778  isclo  23030  ptclsg  23558  ufilcmp  23975  cfilres  25253  ovolgelb  25438  volsup2  25563  vitali  25571  itg1climres  25672  itg2seq  25700  itg2monolem1  25708  itg2mono  25711  itg2i1fseq  25713  itg2cn  25721  ellimc2  25835  rolle  25951  lhop1  25976  itgsubstlem  26012  tdeglem4  26022  mpodvdsmulf1o  27161  dvdsmulf1o  27163  dchrelbas2  27205  selbergsb  27543  axcontlem2  28949  dfconngr1  30174  hodsi  31761  ho01i  31814  ho02i  31815  lnopeqi  31994  nmcopexi  32013  nmcfnexi  32037  cnlnadjlem3  32055  cnlnadjlem5  32057  leop3  32111  pjssposi  32158  largei  32253  mdsl2i  32308  mdsl2bi  32309  elat2  32326  dmdbr5ati  32408  cdj3lem3b  32426  subfacp1lem3  35209  dfso3  35742  phpreu  37633  ptrecube  37649  mblfinlem1  37686  voliunnfl  37693  disjressuc2  38411  fimgmcyc  42524  alephiso2  43549  ntrneiel2  44077  wfac8prim  44994  ismbl3  45982  ismbl4  45989  sge0lefimpt  46419  sbgoldbalt  47762