Theorem ralbiia 2962

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

Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977  ∀wral 2896

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

This theorem depends on definitions:  df-bi 196  df-ral 2901

This theorem is referenced by:  poinxp  5105  soinxp  5106  seinxp  5108  dffun8  5831  funcnv3  5873  fncnv  5876  fnres  5921  fvreseq0  6225  isoini2  6489  smores  7336  tfr3ALT  7385  resixp  7829  ixpfi2  8147  marypha1lem  8222  ac5num  8742  acni2  8752  acndom  8757  dfac4  8828  brdom7disj  9234  brdom6disj  9235  fpwwe2lem8  9338  axgroth6  9529  rabssnn0fi  12647  lo1res  14138  isprm5  15257  prmreclem2  15459  tsrss  17046  gass  17557  efgval2  17960  efgsres  17974  isdomn2  19120  islinds2  19971  isclo  20701  ptclsg  21228  ufilcmp  21646  cfilres  22902  ovolgelb  23055  volsup2  23179  vitali  23188  itg1climres  23287  itg2seq  23315  itg2monolem1  23323  itg2mono  23326  itg2i1fseq  23328  itg2cn  23336  ellimc2  23447  rolle  23557  lhop1  23581  itgsubstlem  23615  tdeglem4  23624  dvdsmulf1o  24720  dchrelbas2  24762  selbergsb  25064  axcontlem2  25645  dfconngra1  26199  hodsi  28018  ho01i  28071  ho02i  28072  lnopeqi  28251  nmcopexi  28270  nmcfnexi  28294  cnlnadjlem3  28312  cnlnadjlem5  28314  leop3  28368  pjssposi  28415  largei  28510  mdsl2i  28565  mdsl2bi  28566  elat2  28583  dmdbr5ati  28665  cdj3lem3b  28683  subfacp1lem3  30418  dfso3  30856  phpreu  32563  ptrecube  32579  mblfinlem1  32616  voliunnfl  32623  acsfn1p  36788  ntrneiel2  37404  ismbl3  38879  ismbl4  38886  sge0lefimpt  39316  sgoldbalt  40203  dfconngr1  41355