Theorem ralbiia 3092

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

Syntax hints:   → wi 4   ↔ wb 205   ∈ wcel 2107  ∀wral 3062

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

This theorem depends on definitions:  df-bi 206  df-ral 3063

This theorem is referenced by:  ralbii  3094  ralanid  3096  poinxp  5754  soinxp  5755  seinxp  5757  dffun8  6573  funcnv3  6615  fncnv  6618  fnres  6674  fvreseq0  7035  isoini2  7331  smores  8347  tfr3ALT  8397  resixp  8923  ixpfi2  9346  marypha1lem  9424  ac5num  10027  acni2  10037  acndom  10042  dfac4  10113  brdom7disj  10522  brdom6disj  10523  fpwwe2lem7  10628  axgroth6  10819  rabssnn0fi  13947  lo1res  15499  isprm5  16640  prmreclem2  16846  tsrss  18538  gass  19159  efgval2  19585  efgsres  19599  acsfn1p  20403  isdomn2  20902  islinds2  21352  isclo  22573  ptclsg  23101  ufilcmp  23518  cfilres  24795  ovolgelb  24979  volsup2  25104  vitali  25112  itg1climres  25214  itg2seq  25242  itg2monolem1  25250  itg2mono  25253  itg2i1fseq  25255  itg2cn  25263  ellimc2  25376  rolle  25489  lhop1  25513  itgsubstlem  25547  tdeglem4  25559  tdeglem4OLD  25560  dvdsmulf1o  26678  dchrelbas2  26720  selbergsb  27058  axcontlem2  28203  dfconngr1  29421  hodsi  31006  ho01i  31059  ho02i  31060  lnopeqi  31239  nmcopexi  31258  nmcfnexi  31282  cnlnadjlem3  31300  cnlnadjlem5  31302  leop3  31356  pjssposi  31403  largei  31498  mdsl2i  31553  mdsl2bi  31554  elat2  31571  dmdbr5ati  31653  cdj3lem3b  31671  subfacp1lem3  34111  dfso3  34627  phpreu  36410  ptrecube  36426  mblfinlem1  36463  voliunnfl  36470  disjressuc2  37196  alephiso2  42242  ntrneiel2  42770  ismbl3  44637  ismbl4  44644  sge0lefimpt  45074  sbgoldbalt  46384