Theorem ralbiia 3085

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 273	. 2 ⊢ ((𝑥 ∈ 𝐴 → 𝜑) ↔ (𝑥 ∈ 𝐴 → 𝜓))
3	2	ralbii2 3083	1 ⊢ (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥 ∈ 𝐴 𝜓)

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2121  ∀wral 3055

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

This theorem depends on definitions:  df-bi 209  df-ral 3056

This theorem is referenced by:  ralbii  3087  ralanid  3089  poinxp  5701  soinxp  5702  seinxp  5704  dffun8  6516  funcnv3  6558  fncnv  6561  fnres  6615  fvreseq0  6982  isoini2  7286  smores  8285  tfr3ALT  8335  resixp  8875  ixpfi2  9254  marypha1lem  9340  ac5num  9953  acni2  9963  acndom  9968  dfac4  10039  brdom7disj  10449  brdom6disj  10450  fpwwe2lem7  10556  axgroth6  10747  rabssnn0fi  13943  lo1res  15516  isprm5  16672  prmreclem2  16883  tsrss  18550  gass  19270  efgval2  19693  efgsres  19707  isdomn2  20686  isdomn2OLD  20687  acsfn1p  20774  islinds2  21791  isclo  23073  ptclsg  23601  ufilcmp  24018  cfilres  25284  ovolgelb  25468  volsup2  25593  vitali  25601  itg1climres  25702  itg2seq  25730  itg2monolem1  25738  itg2mono  25741  itg2i1fseq  25743  itg2cn  25751  ellimc2  25865  rolle  25978  lhop1  26002  itgsubstlem  26036  tdeglem4  26046  mpodvdsmulf1o  27178  dvdsmulf1o  27180  dchrelbas2  27221  selbergsb  27559  axcontlem2  29054  dfconngr1  30278  hodsi  31866  ho01i  31919  ho02i  31920  lnopeqi  32099  nmcopexi  32118  nmcfnexi  32142  cnlnadjlem3  32160  cnlnadjlem5  32162  leop3  32216  pjssposi  32263  largei  32358  mdsl2i  32413  mdsl2bi  32414  elat2  32431  dmdbr5ati  32513  cdj3lem3b  32531  subfacp1lem3  35423  dfso3  35961  phpreu  37984  ptrecube  38000  mblfinlem1  38037  voliunnfl  38044  ralrnmo  38741  raldmqsmo  38743  disjressuc2  38791  fimgmcyc  43033  alephiso2  44015  ntrneiel2  44543  wfac8prim  45459  ismbl3  46441  ismbl4  46448  sge0lefimpt  46878  sbgoldbalt  48284