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  5700  soinxp  5701  seinxp  5703  dffun8  6510  funcnv3  6552  fncnv  6555  fnres  6609  fvreseq0  6972  isoini2  7276  smores  8275  tfr3ALT  8324  resixp  8860  ixpfi2  9240  marypha1lem  9323  ac5num  9930  acni2  9940  acndom  9945  dfac4  10016  brdom7disj  10425  brdom6disj  10426  fpwwe2lem7  10531  axgroth6  10722  rabssnn0fi  13893  lo1res  15466  isprm5  16618  prmreclem2  16829  tsrss  18495  gass  19180  efgval2  19603  efgsres  19617  isdomn2  20596  isdomn2OLD  20597  acsfn1p  20684  islinds2  21720  isclo  22972  ptclsg  23500  ufilcmp  23917  cfilres  25194  ovolgelb  25379  volsup2  25504  vitali  25512  itg1climres  25613  itg2seq  25641  itg2monolem1  25649  itg2mono  25652  itg2i1fseq  25654  itg2cn  25662  ellimc2  25776  rolle  25892  lhop1  25917  itgsubstlem  25953  tdeglem4  25963  mpodvdsmulf1o  27102  dvdsmulf1o  27104  dchrelbas2  27146  selbergsb  27484  axcontlem2  28910  dfconngr1  30132  hodsi  31719  ho01i  31772  ho02i  31773  lnopeqi  31952  nmcopexi  31971  nmcfnexi  31995  cnlnadjlem3  32013  cnlnadjlem5  32015  leop3  32069  pjssposi  32116  largei  32211  mdsl2i  32266  mdsl2bi  32267  elat2  32284  dmdbr5ati  32366  cdj3lem3b  32384  subfacp1lem3  35165  dfso3  35703  phpreu  37594  ptrecube  37610  mblfinlem1  37647  voliunnfl  37654  disjressuc2  38370  fimgmcyc  42517  alephiso2  43541  ntrneiel2  44069  wfac8prim  44986  ismbl3  45977  ismbl4  45984  sge0lefimpt  46414  sbgoldbalt  47775