Theorem raleq12d 1841

Description: Equality deduction for restricted universal quantifier.

Hypotheses

Ref	Expression
raleq12d.1	⊢ (φ → A = B)
raleq12d.2	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
raleq12d	⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))

Distinct variable groups:   x,A   x,B   φ,x

Proof of Theorem raleq12d

Step	Hyp	Ref	Expression
1		raleq12d.1	. . 3 ⊢ (φ → A = B)
2	1	raleq1d 1836	. 2 ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B ψ))
3		raleq12d.2	. . 3 ⊢ (φ → (ψ ↔ χ))
4	3	ralbidv 1710	. 2 ⊢ (φ → (∀x ∈ B ψ ↔ ∀x ∈ B χ))
5	2, 4	bitrd 539	1 ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))

Syntax hints:   → wi 3   ↔ wb 153   = wceq 997  ∀wral 1692

This theorem is referenced by:  climconst3 7186  ishaus 7868  iscms 8031  grpidval 8142  isring 8225  vci 8251  isvclem 8280  isnvlem 8313  nvi 8317  lnoval 8497  ajfval 8553  isphg 8560  spwval2 8737  elghomlem1 10467  vri 10583  isfuna 10838

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-ext 1504

This theorem depends on definitions:  df-bi 154  df-an 232  df-ex 1022  df-cleq 1515  df-clel 1518  df-ral 1696

Copyright terms: Public domain