Theorem bj-unrab

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

	Ref	Expression
Assertion	bj-unrab	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 )
2		rabss2	⊢ ( 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) → { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜑 } )
3	1 2	ax-mp	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜑 }
4		orc	⊢ ( 𝜑 → ( 𝜑 ∨ 𝜓 ) )
5	4	a1i	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → ( 𝜑 → ( 𝜑 ∨ 𝜓 ) ) )
6	5	ss2rabi	⊢ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜑 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }
7	3 6	sstri	⊢ { 𝑥 ∈ 𝐴 ∣ 𝜑 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }
8		ssun2	⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 )
9		rabss2	⊢ ( 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) → { 𝑥 ∈ 𝐵 ∣ 𝜓 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜓 } )
10	8 9	ax-mp	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜓 }
11		olc	⊢ ( 𝜓 → ( 𝜑 ∨ 𝜓 ) )
12	11	a1i	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → ( 𝜓 → ( 𝜑 ∨ 𝜓 ) ) )
13	12	ss2rabi	⊢ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ 𝜓 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }
14	10 13	sstri	⊢ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }
15	7 14	unssi	⊢ ( { 𝑥 ∈ 𝐴 ∣ 𝜑 } ∪ { 𝑥 ∈ 𝐵 ∣ 𝜓 } ) ⊆ { 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ∣ ( 𝜑 ∨ 𝜓 ) }