Theorem ralbiia 3110

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

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

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 3081

This theorem is used by:  ralbii  3112  ralanid  3114  poinxp  5737  soinxp  5738  seinxp  5740  dffun8  6585  funcnv3  6629  fncnv  6632  fnres  6685  fvreseq0  7057  isoini2  7367  smores  8385  tfr3ALT  8435  resixp  8986  ixpfi2  9364  marypha1lem  9449  ac5num  10139  acni2  10149  acndom  10154  dfac4  10225  brdom7disj  10634  brdom6disj  10635  fpwwe2lem7  10746  axgroth6  10937  rabssnn0fi  14153  lo1res  15752  isprm5  16909  prmreclem2  17121  tsrss  18789  gass  19542  efgval2  19965  efgsres  19979  isdomn2  20990  acsfn1p  21083  islinds2  22146  isclo  23432  ptclsg  23961  ufilcmp  24378  cfilres  25644  ovolgelb  25828  volsup2  25953  vitali  25961  itg1climres  26062  itg2seq  26090  itg2monolem1  26098  itg2mono  26101  itg2i1fseq  26103  itg2cn  26111  ellimc2  26224  rolle  26337  lhop1  26361  itgsubstlem  26395  tdeglem4  26405  mpodvdsmulf1o  27548  dvdsmulf1o  27550  dchrelbas2  27591  selbergsb  27929  axcontlem2  29570  dfconngr1  30816  hodsi  32404  ho01i  32457  ho02i  32458  lnopeqi  32637  nmcopexi  32656  nmcfnexi  32680  cnlnadjlem3  32698  cnlnadjlem5  32700  leop3  32754  pjssposi  32801  largei  32896  mdsl2i  32951  mdsl2bi  32952  elat2  32969  dmdbr5ati  33051  cdj3lem3b  33069  subfacp1lem3  36113  dfso3  36662  phpreu  38718  ptrecube  38729  mblfinlem1  38766  voliunnfl  38773  ralrnmo  39484  raldmqsmo  39486  disjressuc2  39534  fimgmcyc  43789  alephiso2  44749  ntrneiel2  45276  wfac8prim  46185  ismbl3  47199  ismbl4  47206  sge0lefimpt  47636  sbgoldbalt  49082