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 3052

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 3053

This theorem is referenced by:  ralbii  3083  ralanid  3085  poinxp  5706  soinxp  5707  seinxp  5709  dffun8  6521  funcnv3  6563  fncnv  6566  fnres  6620  fvreseq0  6985  isoini2  7287  smores  8286  tfr3ALT  8335  resixp  8875  ixpfi2  9254  marypha1lem  9340  ac5num  9950  acni2  9960  acndom  9965  dfac4  10036  brdom7disj  10445  brdom6disj  10446  fpwwe2lem7  10552  axgroth6  10743  rabssnn0fi  13913  lo1res  15486  isprm5  16638  prmreclem2  16849  tsrss  18516  gass  19234  efgval2  19657  efgsres  19671  isdomn2  20648  isdomn2OLD  20649  acsfn1p  20736  islinds2  21772  isclo  23035  ptclsg  23563  ufilcmp  23980  cfilres  25256  ovolgelb  25441  volsup2  25566  vitali  25574  itg1climres  25675  itg2seq  25703  itg2monolem1  25711  itg2mono  25714  itg2i1fseq  25716  itg2cn  25724  ellimc2  25838  rolle  25954  lhop1  25979  itgsubstlem  26015  tdeglem4  26025  mpodvdsmulf1o  27164  dvdsmulf1o  27166  dchrelbas2  27208  selbergsb  27546  axcontlem2  29042  dfconngr1  30267  hodsi  31854  ho01i  31907  ho02i  31908  lnopeqi  32087  nmcopexi  32106  nmcfnexi  32130  cnlnadjlem3  32148  cnlnadjlem5  32150  leop3  32204  pjssposi  32251  largei  32346  mdsl2i  32401  mdsl2bi  32402  elat2  32419  dmdbr5ati  32501  cdj3lem3b  32519  subfacp1lem3  35378  dfso3  35916  phpreu  37807  ptrecube  37823  mblfinlem1  37860  voliunnfl  37867  ralrnmo  38564  raldmqsmo  38566  disjressuc2  38614  fimgmcyc  42856  alephiso2  43866  ntrneiel2  44394  wfac8prim  45310  ismbl3  46297  ismbl4  46304  sge0lefimpt  46734  sbgoldbalt  48094