Theorem unopab

Description: Union of two ordered pair class abstractions. (Contributed by NM, 30-Sep-2002)

	Ref	Expression
Assertion	unopab	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∨ 𝜓 ) }

Proof

Step	Hyp	Ref	Expression
1		unab	⊢ ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } ) = { 𝑧 ∣ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) }
2		19.43	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
3		andi	⊢ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) ↔ ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
4	3	exbii	⊢ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) ↔ ∃ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
5		19.43	⊢ ( ∃ 𝑦 ( ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) )
6	4 5	bitr2i	⊢ ( ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) )
7	6	exbii	⊢ ( ∃ 𝑥 ( ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) )
8	2 7	bitr3i	⊢ ( ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) )
9	8	abbii	⊢ { 𝑧 ∣ ( ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) ∨ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) }
10	1 9	eqtri	⊢ ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } ) = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) }
11		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) }
12		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) }
13	11 12	uneq12i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜑 ) } ∪ { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ 𝜓 ) } )
14		df-opab	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∨ 𝜓 ) } = { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ ∧ ( 𝜑 ∨ 𝜓 ) ) }
15	10 13 14	3eqtr4i	⊢ ( { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜑 } ∪ { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝜓 } ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝜑 ∨ 𝜓 ) }