Theorem ralbiia 3078

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2113  ∀wral 3049

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

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

This theorem is referenced by:  ralbii  3080  ralanid  3082  poinxp  5703  soinxp  5704  seinxp  5706  dffun8  6518  funcnv3  6560  fncnv  6563  fnres  6617  fvreseq0  6981  isoini2  7283  smores  8282  tfr3ALT  8331  resixp  8869  ixpfi2  9248  marypha1lem  9334  ac5num  9944  acni2  9954  acndom  9959  dfac4  10030  brdom7disj  10439  brdom6disj  10440  fpwwe2lem7  10546  axgroth6  10737  rabssnn0fi  13907  lo1res  15480  isprm5  16632  prmreclem2  16843  tsrss  18510  gass  19228  efgval2  19651  efgsres  19665  isdomn2  20642  isdomn2OLD  20643  acsfn1p  20730  islinds2  21766  isclo  23029  ptclsg  23557  ufilcmp  23974  cfilres  25250  ovolgelb  25435  volsup2  25560  vitali  25568  itg1climres  25669  itg2seq  25697  itg2monolem1  25705  itg2mono  25708  itg2i1fseq  25710  itg2cn  25718  ellimc2  25832  rolle  25948  lhop1  25973  itgsubstlem  26009  tdeglem4  26019  mpodvdsmulf1o  27158  dvdsmulf1o  27160  dchrelbas2  27202  selbergsb  27540  axcontlem2  28987  dfconngr1  30212  hodsi  31799  ho01i  31852  ho02i  31853  lnopeqi  32032  nmcopexi  32051  nmcfnexi  32075  cnlnadjlem3  32093  cnlnadjlem5  32095  leop3  32149  pjssposi  32196  largei  32291  mdsl2i  32346  mdsl2bi  32347  elat2  32364  dmdbr5ati  32446  cdj3lem3b  32464  subfacp1lem3  35325  dfso3  35863  phpreu  37744  ptrecube  37760  mblfinlem1  37797  voliunnfl  37804  disjressuc2  38535  fimgmcyc  42731  alephiso2  43741  ntrneiel2  44269  wfac8prim  45185  ismbl3  46172  ismbl4  46179  sge0lefimpt  46609  sbgoldbalt  47969