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 2144  ∀wral 3076

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

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

This theorem is used by:  ralbii  3108  ralanid  3110  poinxp  5731  soinxp  5732  seinxp  5734  dffun8  6568  funcnv3  6610  fncnv  6613  fnres  6666  fvreseq0  7037  isoini2  7347  smores  8360  tfr3ALT  8410  resixp  8961  ixpfi2  9339  marypha1lem  9425  ac5num  10115  acni2  10125  acndom  10130  dfac4  10201  brdom7disj  10610  brdom6disj  10611  fpwwe2lem7  10722  axgroth6  10913  rabssnn0fi  14129  lo1res  15726  isprm5  16883  prmreclem2  17095  tsrss  18763  gass  19515  efgval2  19938  efgsres  19952  isdomn2  20963  acsfn1p  21056  islinds2  22119  isclo  23405  ptclsg  23934  ufilcmp  24351  cfilres  25617  ovolgelb  25801  volsup2  25926  vitali  25934  itg1climres  26035  itg2seq  26063  itg2monolem1  26071  itg2mono  26074  itg2i1fseq  26076  itg2cn  26084  ellimc2  26197  rolle  26310  lhop1  26334  itgsubstlem  26368  tdeglem4  26378  mpodvdsmulf1o  27521  dvdsmulf1o  27523  dchrelbas2  27564  selbergsb  27902  axcontlem2  29543  dfconngr1  30789  hodsi  32377  ho01i  32430  ho02i  32431  lnopeqi  32610  nmcopexi  32629  nmcfnexi  32653  cnlnadjlem3  32671  cnlnadjlem5  32673  leop3  32727  pjssposi  32774  largei  32869  mdsl2i  32924  mdsl2bi  32925  elat2  32942  dmdbr5ati  33024  cdj3lem3b  33042  subfacp1lem3  35947  dfso3  36485  phpreu  38528  ptrecube  38539  mblfinlem1  38576  voliunnfl  38583  ralrnmo  39294  raldmqsmo  39296  disjressuc2  39344  fimgmcyc  43599  alephiso2  44559  ntrneiel2  45086  wfac8prim  45992  ismbl3  46996  ismbl4  47003  sge0lefimpt  47433  sbgoldbalt  48879