Theorem ralbiia 2979

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

Syntax hints:   → wi 4   ↔ wb 196   ∈ wcel 1990  ∀wral 2912

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

This theorem depends on definitions:  df-bi 197  df-ral 2917

This theorem is referenced by:  poinxp  5182  soinxp  5183  seinxp  5185  dffun8  5916  funcnv3  5959  fncnv  5962  fnres  6007  fvreseq0  6317  isoini2  6589  smores  7449  tfr3ALT  7498  resixp  7943  ixpfi2  8264  marypha1lem  8339  ac5num  8859  acni2  8869  acndom  8874  dfac4  8945  brdom7disj  9353  brdom6disj  9354  fpwwe2lem8  9459  axgroth6  9650  rabssnn0fi  12785  lo1res  14290  isprm5  15419  prmreclem2  15621  tsrss  17223  gass  17734  efgval2  18137  efgsres  18151  isdomn2  19299  islinds2  20152  isclo  20891  ptclsg  21418  ufilcmp  21836  cfilres  23094  ovolgelb  23248  volsup2  23373  vitali  23382  itg1climres  23481  itg2seq  23509  itg2monolem1  23517  itg2mono  23520  itg2i1fseq  23522  itg2cn  23530  ellimc2  23641  rolle  23753  lhop1  23777  itgsubstlem  23811  tdeglem4  23820  dvdsmulf1o  24920  dchrelbas2  24962  selbergsb  25264  axcontlem2  25845  dfconngr1  27048  hodsi  28634  ho01i  28687  ho02i  28688  lnopeqi  28867  nmcopexi  28886  nmcfnexi  28910  cnlnadjlem3  28928  cnlnadjlem5  28930  leop3  28984  pjssposi  29031  largei  29126  mdsl2i  29181  mdsl2bi  29182  elat2  29199  dmdbr5ati  29281  cdj3lem3b  29299  subfacp1lem3  31164  dfso3  31601  phpreu  33393  ptrecube  33409  mblfinlem1  33446  voliunnfl  33453  acsfn1p  37769  ntrneiel2  38384  ismbl3  40203  ismbl4  40210  sge0lefimpt  40640  sbgoldbalt  41669