This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem raldifeq

Description: Equality theorem for restricted universal quantifier. (Contributed by Thierry Arnoux, 6-Jul-2019)

Ref Expression
Hypotheses raldifeq.1 ⊢ φ → A ⊆ B
raldifeq.2 ⊢ φ → ∀ x ∈ B ∖ A ψ
Assertion raldifeq ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ

Proof

Step Hyp Ref Expression
1 raldifeq.1 ⊢ φ → A ⊆ B
2 raldifeq.2 ⊢ φ → ∀ x ∈ B ∖ A ψ
3 2 biantrud ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A ψ ∧ ∀ x ∈ B ∖ A ψ
4 ralunb ⊢ ∀ x ∈ A ∪ B ∖ A ψ ↔ ∀ x ∈ A ψ ∧ ∀ x ∈ B ∖ A ψ
5 3 4 bitr4di ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ A ∪ B ∖ A ψ
6 undif ⊢ A ⊆ B ↔ A ∪ B ∖ A = B
7 1 6 sylib ⊢ φ → A ∪ B ∖ A = B
8 7 raleqdv ⊢ φ → ∀ x ∈ A ∪ B ∖ A ψ ↔ ∀ x ∈ B ψ
9 5 8 bitrd ⊢ φ → ∀ x ∈ A ψ ↔ ∀ x ∈ B ψ