Theorem ralbiia 3081

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2114  ∀wral 3051

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 207  df-ral 3052

This theorem is referenced by:  ralbii  3083  ralanid  3085  poinxp  5712  soinxp  5713  seinxp  5715  dffun8  6526  funcnv3  6568  fncnv  6571  fnres  6625  fvreseq0  6990  isoini2  7294  smores  8292  tfr3ALT  8341  resixp  8881  ixpfi2  9260  marypha1lem  9346  ac5num  9958  acni2  9968  acndom  9973  dfac4  10044  brdom7disj  10453  brdom6disj  10454  fpwwe2lem7  10560  axgroth6  10751  rabssnn0fi  13948  lo1res  15521  isprm5  16677  prmreclem2  16888  tsrss  18555  gass  19276  efgval2  19699  efgsres  19713  isdomn2  20688  isdomn2OLD  20689  acsfn1p  20776  islinds2  21793  isclo  23052  ptclsg  23580  ufilcmp  23997  cfilres  25263  ovolgelb  25447  volsup2  25572  vitali  25580  itg1climres  25681  itg2seq  25709  itg2monolem1  25717  itg2mono  25720  itg2i1fseq  25722  itg2cn  25730  ellimc2  25844  rolle  25957  lhop1  25981  itgsubstlem  26015  tdeglem4  26025  mpodvdsmulf1o  27157  dvdsmulf1o  27159  dchrelbas2  27200  selbergsb  27538  axcontlem2  29034  dfconngr1  30258  hodsi  31846  ho01i  31899  ho02i  31900  lnopeqi  32079  nmcopexi  32098  nmcfnexi  32122  cnlnadjlem3  32140  cnlnadjlem5  32142  leop3  32196  pjssposi  32243  largei  32338  mdsl2i  32393  mdsl2bi  32394  elat2  32411  dmdbr5ati  32493  cdj3lem3b  32511  subfacp1lem3  35364  dfso3  35902  phpreu  37925  ptrecube  37941  mblfinlem1  37978  voliunnfl  37985  ralrnmo  38682  raldmqsmo  38684  disjressuc2  38732  fimgmcyc  42979  alephiso2  43985  ntrneiel2  44513  wfac8prim  45429  ismbl3  46414  ismbl4  46421  sge0lefimpt  46851  sbgoldbalt  48257