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  5712  soinxp  5713  seinxp  5715  dffun8  6528  funcnv3  6570  fncnv  6573  fnres  6627  fvreseq0  6992  isoini2  7296  smores  8298  tfr3ALT  8347  resixp  8883  ixpfi2  9277  marypha1lem  9360  ac5num  9965  acni2  9975  acndom  9980  dfac4  10051  brdom7disj  10460  brdom6disj  10461  fpwwe2lem7  10566  axgroth6  10757  rabssnn0fi  13927  lo1res  15501  isprm5  16653  prmreclem2  16864  tsrss  18530  gass  19215  efgval2  19638  efgsres  19652  isdomn2  20631  isdomn2OLD  20632  acsfn1p  20719  islinds2  21755  isclo  23007  ptclsg  23535  ufilcmp  23952  cfilres  25229  ovolgelb  25414  volsup2  25539  vitali  25547  itg1climres  25648  itg2seq  25676  itg2monolem1  25684  itg2mono  25687  itg2i1fseq  25689  itg2cn  25697  ellimc2  25811  rolle  25927  lhop1  25952  itgsubstlem  25988  tdeglem4  25998  mpodvdsmulf1o  27137  dvdsmulf1o  27139  dchrelbas2  27181  selbergsb  27519  axcontlem2  28945  dfconngr1  30167  hodsi  31754  ho01i  31807  ho02i  31808  lnopeqi  31987  nmcopexi  32006  nmcfnexi  32030  cnlnadjlem3  32048  cnlnadjlem5  32050  leop3  32104  pjssposi  32151  largei  32246  mdsl2i  32301  mdsl2bi  32302  elat2  32319  dmdbr5ati  32401  cdj3lem3b  32419  subfacp1lem3  35162  dfso3  35700  phpreu  37591  ptrecube  37607  mblfinlem1  37644  voliunnfl  37651  disjressuc2  38367  fimgmcyc  42515  alephiso2  43540  ntrneiel2  44068  wfac8prim  44985  ismbl3  45977  ismbl4  45984  sge0lefimpt  46414  sbgoldbalt  47775