Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - start with the Axiom of Extensionality
Ordered-pair class abstractions (class builders)
unopab
Next ⟩
Functions in maps-to notation
Metamath Proof Explorer
Ascii
Unicode
Theorem
unopab
Description:
Union of two ordered pair class abstractions.
(Contributed by
NM
, 30-Sep-2002)
Ref
Expression
Assertion
unopab
⊢
x
y
|
φ
∪
x
y
|
ψ
=
x
y
|
φ
∨
ψ
Proof
Step
Hyp
Ref
Expression
1
unab
⊢
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∪
z
|
∃
x
∃
y
z
=
x
y
∧
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
x
∃
y
z
=
x
y
∧
ψ
2
19.43
⊢
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
y
z
=
x
y
∧
ψ
↔
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
x
∃
y
z
=
x
y
∧
ψ
3
andi
⊢
z
=
x
y
∧
φ
∨
ψ
↔
z
=
x
y
∧
φ
∨
z
=
x
y
∧
ψ
4
3
exbii
⊢
∃
y
z
=
x
y
∧
φ
∨
ψ
↔
∃
y
z
=
x
y
∧
φ
∨
z
=
x
y
∧
ψ
5
19.43
⊢
∃
y
z
=
x
y
∧
φ
∨
z
=
x
y
∧
ψ
↔
∃
y
z
=
x
y
∧
φ
∨
∃
y
z
=
x
y
∧
ψ
6
4
5
bitr2i
⊢
∃
y
z
=
x
y
∧
φ
∨
∃
y
z
=
x
y
∧
ψ
↔
∃
y
z
=
x
y
∧
φ
∨
ψ
7
6
exbii
⊢
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
y
z
=
x
y
∧
ψ
↔
∃
x
∃
y
z
=
x
y
∧
φ
∨
ψ
8
2
7
bitr3i
⊢
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
x
∃
y
z
=
x
y
∧
ψ
↔
∃
x
∃
y
z
=
x
y
∧
φ
∨
ψ
9
8
abbii
⊢
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∨
∃
x
∃
y
z
=
x
y
∧
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∨
ψ
10
1
9
eqtri
⊢
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∪
z
|
∃
x
∃
y
z
=
x
y
∧
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∨
ψ
11
df-opab
⊢
x
y
|
φ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
12
df-opab
⊢
x
y
|
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
ψ
13
11
12
uneq12i
⊢
x
y
|
φ
∪
x
y
|
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∪
z
|
∃
x
∃
y
z
=
x
y
∧
ψ
14
df-opab
⊢
x
y
|
φ
∨
ψ
=
z
|
∃
x
∃
y
z
=
x
y
∧
φ
∨
ψ
15
10
13
14
3eqtr4i
⊢
x
y
|
φ
∪
x
y
|
ψ
=
x
y
|
φ
∨
ψ