Theorem ralbiia 1720

Description: Inference adding restricted universal quantifier to both sides of an equivalence.

Hypothesis

Ref	Expression
ralbiia.1	⊢ (x ∈ A → (φ ↔ ψ))

Assertion

Ref	Expression
ralbiia	⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)

Proof of Theorem ralbiia

Step	Hyp	Ref	Expression
1		ralbiia.1	. . 3 ⊢ (x ∈ A → (φ ↔ ψ))
2	1	pm5.74i 595	. 2 ⊢ ((x ∈ A → φ) ↔ (x ∈ A → ψ))
3	2	ralbii2 1718	1 ⊢ (∀x ∈ A φ ↔ ∀x ∈ A ψ)

Syntax hints:   → wi 3   ↔ wb 153   ∈ wcel 999  ∀wral 1692

This theorem is referenced by:  funcnv3 3615  fncnv 3618  fvreseq 3856  aceq4 4796  brdom7disj 4866  brdom6disj 4867  iundom 4874  cau2i 7003  clmnnsi 7174  climresi 7195  climshft2i 7196  isumnn0nnai 7298  isummulc1ai 7304  cvgratlem3ALT 7339  cvgratlem3 7342  negfcncfi 7359  efaddlem27 7454  metreslem 7907  lmbrnns 8027  lmcvgnns 8028  hodsi 9784  ho01i 9837  ho02i 9838  lnopeqi 10016  nmcopexlem2 10035  lnopconi 10046  nmcfnexlem2 10064  lnfnconi 10073  cnlnadjlem3 10085  cnlnadjlem4 10086  cnlnadjlem5 10087  leop3 10141  pjssposi 10183  largei 10278  mdsl2i 10333  mdsl2bi 10334  elat2 10351  dmdbr5ati 10433  cdj3lem3b 10451

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 1004  ax-4 1014  ax-5o 1016

This theorem depends on definitions:  df-bi 154  df-an 232  df-ral 1696

Copyright terms: Public domain