Theorem ralbiia 3097

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2108  ∀wral 3067

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

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

This theorem is referenced by:  ralbii  3099  ralanid  3101  poinxp  5780  soinxp  5781  seinxp  5783  dffun8  6606  funcnv3  6648  fncnv  6651  fnres  6707  fvreseq0  7071  isoini2  7375  smores  8408  tfr3ALT  8458  resixp  8991  ixpfi2  9420  marypha1lem  9502  ac5num  10105  acni2  10115  acndom  10120  dfac4  10191  brdom7disj  10600  brdom6disj  10601  fpwwe2lem7  10706  axgroth6  10897  rabssnn0fi  14037  lo1res  15605  isprm5  16754  prmreclem2  16964  tsrss  18659  gass  19341  efgval2  19766  efgsres  19780  isdomn2  20733  isdomn2OLD  20734  acsfn1p  20822  islinds2  21856  isclo  23116  ptclsg  23644  ufilcmp  24061  cfilres  25349  ovolgelb  25534  volsup2  25659  vitali  25667  itg1climres  25769  itg2seq  25797  itg2monolem1  25805  itg2mono  25808  itg2i1fseq  25810  itg2cn  25818  ellimc2  25932  rolle  26048  lhop1  26073  itgsubstlem  26109  tdeglem4  26119  mpodvdsmulf1o  27255  dvdsmulf1o  27257  dchrelbas2  27299  selbergsb  27637  axcontlem2  28998  dfconngr1  30220  hodsi  31807  ho01i  31860  ho02i  31861  lnopeqi  32040  nmcopexi  32059  nmcfnexi  32083  cnlnadjlem3  32101  cnlnadjlem5  32103  leop3  32157  pjssposi  32204  largei  32299  mdsl2i  32354  mdsl2bi  32355  elat2  32372  dmdbr5ati  32454  cdj3lem3b  32472  subfacp1lem3  35150  dfso3  35682  phpreu  37564  ptrecube  37580  mblfinlem1  37617  voliunnfl  37624  disjressuc2  38344  fimgmcyc  42489  alephiso2  43520  ntrneiel2  44048  ismbl3  45907  ismbl4  45914  sge0lefimpt  46344  sbgoldbalt  47655