Metamath Proof Explorer

Theorem bj-unrab

Description: Generalization of unrab . Equality need not hold. (Contributed by BJ, 21-Apr-2019)

Ref Expression
Assertion bj-unrab ⊢ x ∈ A | φ ∪ x ∈ B | ψ ⊆ x ∈ A ∪ B | φ ∨ ψ

Proof

Step Hyp Ref Expression
1 ssun1 ⊢ A ⊆ A ∪ B
2 rabss2 ⊢ A ⊆ A ∪ B → x ∈ A | φ ⊆ x ∈ A ∪ B | φ
3 1 2 ax-mp ⊢ x ∈ A | φ ⊆ x ∈ A ∪ B | φ
4 orc ⊢ φ → φ ∨ ψ
5 4 a1i ⊢ x ∈ A ∪ B → φ → φ ∨ ψ
6 5 ss2rabi ⊢ x ∈ A ∪ B | φ ⊆ x ∈ A ∪ B | φ ∨ ψ
7 3 6 sstri ⊢ x ∈ A | φ ⊆ x ∈ A ∪ B | φ ∨ ψ
8 ssun2 ⊢ B ⊆ A ∪ B
9 rabss2 ⊢ B ⊆ A ∪ B → x ∈ B | ψ ⊆ x ∈ A ∪ B | ψ
10 8 9 ax-mp ⊢ x ∈ B | ψ ⊆ x ∈ A ∪ B | ψ
11 olc ⊢ ψ → φ ∨ ψ
12 11 a1i ⊢ x ∈ A ∪ B → ψ → φ ∨ ψ
13 12 ss2rabi ⊢ x ∈ A ∪ B | ψ ⊆ x ∈ A ∪ B | φ ∨ ψ
14 10 13 sstri ⊢ x ∈ B | ψ ⊆ x ∈ A ∪ B | φ ∨ ψ
15 7 14 unssi ⊢ x ∈ A | φ ∪ x ∈ B | ψ ⊆ x ∈ A ∪ B | φ ∨ ψ