Theorem ralbiia 3108

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

Syntax hints:   → wi 4   ↔ wb 208   ∈ wcel 2144  ∀wral 3078

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

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

This theorem is referenced by:  ralbii  3110  ralanid  3112  poinxp  5730  soinxp  5731  seinxp  5733  dffun8  6551  funcnv3  6593  fncnv  6596  fnres  6650  fvreseq0  7021  isoini2  7325  smores  8325  tfr3ALT  8375  resixp  8917  ixpfi2  9295  marypha1lem  9381  ac5num  9994  acni2  10004  acndom  10009  dfac4  10080  brdom7disj  10490  brdom6disj  10491  fpwwe2lem7  10597  axgroth6  10788  rabssnn0fi  14001  lo1res  15588  isprm5  16744  prmreclem2  16955  tsrss  18623  gass  19343  efgval2  19766  efgsres  19780  isdomn2  20763  isdomn2OLD  20764  acsfn1p  20850  islinds2  21867  isclo  23149  ptclsg  23677  ufilcmp  24094  cfilres  25360  ovolgelb  25544  volsup2  25669  vitali  25677  itg1climres  25778  itg2seq  25806  itg2monolem1  25814  itg2mono  25817  itg2i1fseq  25819  itg2cn  25827  ellimc2  25941  rolle  26054  lhop1  26078  itgsubstlem  26112  tdeglem4  26122  mpodvdsmulf1o  27260  dvdsmulf1o  27262  dchrelbas2  27303  selbergsb  27641  axcontlem2  29168  dfconngr1  30392  hodsi  31980  ho01i  32033  ho02i  32034  lnopeqi  32213  nmcopexi  32232  nmcfnexi  32256  cnlnadjlem3  32274  cnlnadjlem5  32276  leop3  32330  pjssposi  32377  largei  32472  mdsl2i  32527  mdsl2bi  32528  elat2  32545  dmdbr5ati  32627  cdj3lem3b  32645  subfacp1lem3  35537  dfso3  36075  phpreu  38108  ptrecube  38124  mblfinlem1  38161  voliunnfl  38168  ralrnmo  38865  raldmqsmo  38867  disjressuc2  38915  fimgmcyc  43157  alephiso2  44139  ntrneiel2  44667  wfac8prim  45583  ismbl3  46565  ismbl4  46572  sge0lefimpt  47002  sbgoldbalt  48408