Metamath Proof Explorer

Theorem 2ralunsn

Description: Double restricted quantification over the union of a set and a singleton, using implicit substitution. (Contributed by Paul Chapman, 17-Nov-2012)

Ref Expression
Hypotheses 2ralunsn.1 ⊢ x = B → φ ↔ χ
2ralunsn.2 ⊢ y = B → φ ↔ ψ
2ralunsn.3 ⊢ x = B → ψ ↔ θ
Assertion 2ralunsn ⊢ B ∈ C → ∀ x ∈ A ∪ B ∀ y ∈ A ∪ B φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ y ∈ A χ ∧ θ

Proof

Step Hyp Ref Expression
1 2ralunsn.1 ⊢ x = B → φ ↔ χ
2 2ralunsn.2 ⊢ y = B → φ ↔ ψ
3 2ralunsn.3 ⊢ x = B → ψ ↔ θ
4 2 ralunsn ⊢ B ∈ C → ∀ y ∈ A ∪ B φ ↔ ∀ y ∈ A φ ∧ ψ
5 4 ralbidv ⊢ B ∈ C → ∀ x ∈ A ∪ B ∀ y ∈ A ∪ B φ ↔ ∀ x ∈ A ∪ B ∀ y ∈ A φ ∧ ψ
6 1 ralbidv ⊢ x = B → ∀ y ∈ A φ ↔ ∀ y ∈ A χ
7 6 3 anbi12d ⊢ x = B → ∀ y ∈ A φ ∧ ψ ↔ ∀ y ∈ A χ ∧ θ
8 7 ralunsn ⊢ B ∈ C → ∀ x ∈ A ∪ B ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ∧ ∀ y ∈ A χ ∧ θ
9 r19.26 ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ∀ x ∈ A ψ
10 9 anbi1i ⊢ ∀ x ∈ A ∀ y ∈ A φ ∧ ψ ∧ ∀ y ∈ A χ ∧ θ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ y ∈ A χ ∧ θ
11 8 10 bitrdi ⊢ B ∈ C → ∀ x ∈ A ∪ B ∀ y ∈ A φ ∧ ψ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ y ∈ A χ ∧ θ
12 5 11 bitrd ⊢ B ∈ C → ∀ x ∈ A ∪ B ∀ y ∈ A ∪ B φ ↔ ∀ x ∈ A ∀ y ∈ A φ ∧ ∀ x ∈ A ψ ∧ ∀ y ∈ A χ ∧ θ