Theorem ralbiia 3090

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2107  ∀wral 3060

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

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

This theorem is referenced by:  ralbii  3092  ralanid  3094  poinxp  5765  soinxp  5766  seinxp  5768  dffun8  6593  funcnv3  6635  fncnv  6638  fnres  6694  fvreseq0  7057  isoini2  7360  smores  8393  tfr3ALT  8443  resixp  8974  ixpfi2  9391  marypha1lem  9474  ac5num  10077  acni2  10087  acndom  10092  dfac4  10163  brdom7disj  10572  brdom6disj  10573  fpwwe2lem7  10678  axgroth6  10869  rabssnn0fi  14028  lo1res  15596  isprm5  16745  prmreclem2  16956  tsrss  18635  gass  19320  efgval2  19743  efgsres  19757  isdomn2  20712  isdomn2OLD  20713  acsfn1p  20801  islinds2  21834  isclo  23096  ptclsg  23624  ufilcmp  24041  cfilres  25331  ovolgelb  25516  volsup2  25641  vitali  25649  itg1climres  25750  itg2seq  25778  itg2monolem1  25786  itg2mono  25789  itg2i1fseq  25791  itg2cn  25799  ellimc2  25913  rolle  26029  lhop1  26054  itgsubstlem  26090  tdeglem4  26100  mpodvdsmulf1o  27238  dvdsmulf1o  27240  dchrelbas2  27282  selbergsb  27620  axcontlem2  28981  dfconngr1  30208  hodsi  31795  ho01i  31848  ho02i  31849  lnopeqi  32028  nmcopexi  32047  nmcfnexi  32071  cnlnadjlem3  32089  cnlnadjlem5  32091  leop3  32145  pjssposi  32192  largei  32287  mdsl2i  32342  mdsl2bi  32343  elat2  32360  dmdbr5ati  32442  cdj3lem3b  32460  subfacp1lem3  35188  dfso3  35721  phpreu  37612  ptrecube  37628  mblfinlem1  37665  voliunnfl  37672  disjressuc2  38390  fimgmcyc  42549  alephiso2  43576  ntrneiel2  44104  wfac8prim  45024  ismbl3  46006  ismbl4  46013  sge0lefimpt  46443  sbgoldbalt  47773