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χ∧θ