Theorem ralbiia 3107

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2141  ∀wral 3077

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

This theorem depends on definitions:  df-bi 210  df-ral 3078

This theorem is referenced by:  ralbii  3109  ralanid  3111  poinxp  5742  soinxp  5743  seinxp  5745  dffun8  6564  funcnv3  6606  fncnv  6609  fnres  6662  fvreseq0  7033  isoini2  7337  smores  8338  tfr3ALT  8388  resixp  8930  ixpfi2  9306  marypha1lem  9392  ac5num  10019  acni2  10029  acndom  10034  dfac4  10105  brdom7disj  10514  brdom6disj  10515  fpwwe2lem7  10621  axgroth6  10812  rabssnn0fi  14021  lo1res  15609  isprm5  16765  prmreclem2  16976  tsrss  18644  gass  19370  efgval2  19793  efgsres  19807  isdomn2  20795  acsfn1p  20881  islinds2  21942  isclo  23223  ptclsg  23751  ufilcmp  24168  cfilres  25434  ovolgelb  25618  volsup2  25743  vitali  25751  itg1climres  25852  itg2seq  25880  itg2monolem1  25888  itg2mono  25891  itg2i1fseq  25893  itg2cn  25901  ellimc2  26015  rolle  26128  lhop1  26152  itgsubstlem  26186  tdeglem4  26196  mpodvdsmulf1o  27334  dvdsmulf1o  27336  dchrelbas2  27377  selbergsb  27715  axcontlem2  29281  dfconngr1  30505  hodsi  32093  ho01i  32146  ho02i  32147  lnopeqi  32326  nmcopexi  32345  nmcfnexi  32369  cnlnadjlem3  32387  cnlnadjlem5  32389  leop3  32443  pjssposi  32490  largei  32585  mdsl2i  32640  mdsl2bi  32641  elat2  32658  dmdbr5ati  32740  cdj3lem3b  32758  subfacp1lem3  35628  dfso3  36166  phpreu  38199  ptrecube  38215  mblfinlem1  38252  voliunnfl  38259  ralrnmo  38956  raldmqsmo  38958  disjressuc2  39006  fimgmcyc  43250  alephiso2  44232  ntrneiel2  44760  wfac8prim  45659  ismbl3  46648  ismbl4  46655  sge0lefimpt  47085  sbgoldbalt  48491