Theorem ralbiia 3132

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

Syntax hints:   → wi 4   ↔ wb 209   ∈ wcel 2111  ∀wral 3106

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

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

This theorem is referenced by:  ralanid  3136  poinxp  5596  soinxp  5597  seinxp  5599  dffun8  6352  funcnv3  6394  fncnv  6397  fnres  6446  fvreseq0  6785  isoini2  7071  smores  7972  tfr3ALT  8021  resixp  8480  ixpfi2  8806  marypha1lem  8881  ac5num  9447  acni2  9457  acndom  9462  dfac4  9533  brdom7disj  9942  brdom6disj  9943  fpwwe2lem8  10048  axgroth6  10239  rabssnn0fi  13349  lo1res  14908  isprm5  16041  prmreclem2  16243  tsrss  17825  gass  18423  efgval2  18842  efgsres  18856  acsfn1p  19571  isdomn2  20065  islinds2  20502  isclo  21692  ptclsg  22220  ufilcmp  22637  cfilres  23900  ovolgelb  24084  volsup2  24209  vitali  24217  itg1climres  24318  itg2seq  24346  itg2monolem1  24354  itg2mono  24357  itg2i1fseq  24359  itg2cn  24367  ellimc2  24480  rolle  24593  lhop1  24617  itgsubstlem  24651  tdeglem4  24661  dvdsmulf1o  25779  dchrelbas2  25821  selbergsb  26159  axcontlem2  26759  dfconngr1  27973  hodsi  29558  ho01i  29611  ho02i  29612  lnopeqi  29791  nmcopexi  29810  nmcfnexi  29834  cnlnadjlem3  29852  cnlnadjlem5  29854  leop3  29908  pjssposi  29955  largei  30050  mdsl2i  30105  mdsl2bi  30106  elat2  30123  dmdbr5ati  30205  cdj3lem3b  30223  subfacp1lem3  32542  dfso3  33063  phpreu  35041  ptrecube  35057  mblfinlem1  35094  voliunnfl  35101  alephiso2  40257  ntrneiel2  40789  ismbl3  42628  ismbl4  42635  sge0lefimpt  43062  sbgoldbalt  44299