Theorem ralbiia 3073

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

Syntax hints:   → wi 4   ↔ wb 206   ∈ wcel 2109  ∀wral 3044

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

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

This theorem is referenced by:  ralbii  3075  ralanid  3077  poinxp  5719  soinxp  5720  seinxp  5722  dffun8  6544  funcnv3  6586  fncnv  6589  fnres  6645  fvreseq0  7010  isoini2  7314  smores  8321  tfr3ALT  8370  resixp  8906  ixpfi2  9301  marypha1lem  9384  ac5num  9989  acni2  9999  acndom  10004  dfac4  10075  brdom7disj  10484  brdom6disj  10485  fpwwe2lem7  10590  axgroth6  10781  rabssnn0fi  13951  lo1res  15525  isprm5  16677  prmreclem2  16888  tsrss  18548  gass  19233  efgval2  19654  efgsres  19668  isdomn2  20620  isdomn2OLD  20621  acsfn1p  20708  islinds2  21722  isclo  22974  ptclsg  23502  ufilcmp  23919  cfilres  25196  ovolgelb  25381  volsup2  25506  vitali  25514  itg1climres  25615  itg2seq  25643  itg2monolem1  25651  itg2mono  25654  itg2i1fseq  25656  itg2cn  25664  ellimc2  25778  rolle  25894  lhop1  25919  itgsubstlem  25955  tdeglem4  25965  mpodvdsmulf1o  27104  dvdsmulf1o  27106  dchrelbas2  27148  selbergsb  27486  axcontlem2  28892  dfconngr1  30117  hodsi  31704  ho01i  31757  ho02i  31758  lnopeqi  31937  nmcopexi  31956  nmcfnexi  31980  cnlnadjlem3  31998  cnlnadjlem5  32000  leop3  32054  pjssposi  32101  largei  32196  mdsl2i  32251  mdsl2bi  32252  elat2  32269  dmdbr5ati  32351  cdj3lem3b  32369  subfacp1lem3  35169  dfso3  35707  phpreu  37598  ptrecube  37614  mblfinlem1  37651  voliunnfl  37658  disjressuc2  38374  fimgmcyc  42522  alephiso2  43547  ntrneiel2  44075  wfac8prim  44992  ismbl3  45984  ismbl4  45991  sge0lefimpt  46421  sbgoldbalt  47779