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 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
raldifeq.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝜓 )
Assertion raldifeq ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )

Proof

Step Hyp Ref Expression
1 raldifeq.1 ⊢ ( 𝜑 → 𝐴 ⊆ 𝐵 )
2 raldifeq.2 ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝜓 )
3 2 biantrud ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝜓 ) ) )
4 ralunb ⊢ ( ∀ 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝜓 ↔ ( ∀ 𝑥 ∈ 𝐴 𝜓 ∧ ∀ 𝑥 ∈ ( 𝐵 ∖ 𝐴 ) 𝜓 ) )
5 3 4 bitr4di ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝜓 ) )
6 undif ⊢ ( 𝐴 ⊆ 𝐵 ↔ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
7 1 6 sylib ⊢ ( 𝜑 → ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) = 𝐵 )
8 7 raleqdv ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( 𝐴 ∪ ( 𝐵 ∖ 𝐴 ) ) 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )
9 5 8 bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝐴 𝜓 ↔ ∀ 𝑥 ∈ 𝐵 𝜓 ) )