Theorem ralbiia 3106

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∈ wcel 2145  ∀wral 3076

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842

This proof depends on definitions:  df-bi 210  df-ral 3077

This theorem is used by:  ralbii  3108  ralanid  3110  poinxp  5729  soinxp  5730  seinxp  5732  dffun8  6557  funcnv3  6599  fncnv  6602  fnres  6655  fvreseq0  7026  isoini2  7336  smores  8339  tfr3ALT  8389  resixp  8940  ixpfi2  9317  marypha1lem  9403  ac5num  10072  acni2  10082  acndom  10087  dfac4  10158  brdom7disj  10567  brdom6disj  10568  fpwwe2lem7  10679  axgroth6  10870  rabssnn0fi  14083  lo1res  15679  isprm5  16831  prmreclem2  17042  tsrss  18710  gass  19462  efgval2  19885  efgsres  19899  isdomn2  20910  acsfn1p  21003  islinds2  22066  isclo  23352  ptclsg  23881  ufilcmp  24298  cfilres  25564  ovolgelb  25748  volsup2  25873  vitali  25881  itg1climres  25982  itg2seq  26010  itg2monolem1  26018  itg2mono  26021  itg2i1fseq  26023  itg2cn  26031  ellimc2  26144  rolle  26257  lhop1  26281  itgsubstlem  26315  tdeglem4  26325  mpodvdsmulf1o  27470  dvdsmulf1o  27472  dchrelbas2  27513  selbergsb  27851  axcontlem2  29462  dfconngr1  30708  hodsi  32296  ho01i  32349  ho02i  32350  lnopeqi  32529  nmcopexi  32548  nmcfnexi  32572  cnlnadjlem3  32590  cnlnadjlem5  32592  leop3  32646  pjssposi  32693  largei  32788  mdsl2i  32843  mdsl2bi  32844  elat2  32861  dmdbr5ati  32943  cdj3lem3b  32961  subfacp1lem3  35862  dfso3  36400  phpreu  38441  ptrecube  38452  mblfinlem1  38489  voliunnfl  38496  ralrnmo  39207  raldmqsmo  39209  disjressuc2  39257  fimgmcyc  43514  alephiso2  44496  ntrneiel2  45024  wfac8prim  45923  ismbl3  46912  ismbl4  46919  sge0lefimpt  47349  sbgoldbalt  48795