This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - start with the Axiom of Extensionality The difference, union, and intersection of two classes Class abstractions with difference, union, and intersection of two classes unabw
Description: Union of two class abstractions. Version of unab using implicit
substitution, which does not require ax-8 , ax-10 , ax-12 .
(Contributed by GG , 15-Oct-2024)
Ref
Expression
Hypotheses
unabw.1 ⊢ x = y → φ ↔ χ
unabw.2 ⊢ x = y → ψ ↔ θ
Assertion
unabw ⊢ x | φ ∪ x | ψ = y | χ ∨ θ
Proof
Step
Hyp
Ref
Expression
1
unabw.1 ⊢ x = y → φ ↔ χ
2
unabw.2 ⊢ x = y → ψ ↔ θ
3
df-un ⊢ x | φ ∪ x | ψ = y | y ∈ x | φ ∨ y ∈ x | ψ
4
df-clab ⊢ y ∈ x | φ ↔ y x φ
5
1
sbievw ⊢ y x φ ↔ χ
6
4 5
bitri ⊢ y ∈ x | φ ↔ χ
7
df-clab ⊢ y ∈ x | ψ ↔ y x ψ
8
2
sbievw ⊢ y x ψ ↔ θ
9
7 8
bitri ⊢ y ∈ x | ψ ↔ θ
10
6 9
orbi12i ⊢ y ∈ x | φ ∨ y ∈ x | ψ ↔ χ ∨ θ
11
10
abbii ⊢ y | y ∈ x | φ ∨ y ∈ x | ψ = y | χ ∨ θ
12
3 11
eqtri ⊢ x | φ ∪ x | ψ = y | χ ∨ θ