Theorem ralbidv2 1668

Description: Formula-building rule for restricted universal quantifier (deduction rule).

Hypothesis

Ref	Expression
ralbidv2.1	⊢ (φ → ((x ∈ A → ψ) ↔ (x ∈ B → χ)))

Assertion

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

Distinct variable group:   φ,x

Proof of Theorem ralbidv2

Step	Hyp	Ref	Expression
1		ralbidv2.1	. . 3 ⊢ (φ → ((x ∈ A → ψ) ↔ (x ∈ B → χ)))
2	1	albidv 1280	. 2 ⊢ (φ → (∀x(x ∈ A → ψ) ↔ ∀x(x ∈ B → χ)))
3		df-ral 1652	. 2 ⊢ (∀x ∈ A ψ ↔ ∀x(x ∈ A → ψ))
4		df-ral 1652	. 2 ⊢ (∀x ∈ B χ ↔ ∀x(x ∈ B → χ))
5	2, 3, 4	3bitr4g 557	1 ⊢ (φ → (∀x ∈ A ψ ↔ ∀x ∈ B χ))

Syntax hints:   → wi 3   ↔ wb 146  ∀wal 956   ∈ wcel 960  ∀wral 1648

This theorem is referenced by:  oneqmini 3023  ordunisuc2 3121  oaabs 4258  zorn2lem1 4798  iscard2 4865  supxrre 6085  raluz 6443  efcn 7423  metcnplem 7883  cncfmet 7902  ist1 10585  isded 10640  dedi 10641  iscat 10658  cati 10659  isfuna 10725

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-gen 965  ax-17 973  ax-4 975  ax-5o 977

This theorem depends on definitions:  df-bi 147  df-an 225  df-ral 1652

Copyright terms: Public domain