This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 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 -> ( ph <-> ch ) )
unabw.2 
|- ( x = y -> ( ps <-> th ) )
Assertion unabw 
|- ( { x | ph } u. { x | ps } ) = { y | ( ch \/ th ) }

Proof

Step Hyp Ref Expression
1 unabw.1 
 |-  ( x = y -> ( ph <-> ch ) )
2 unabw.2 
 |-  ( x = y -> ( ps <-> th ) )
3 df-un 
 |-  ( { x | ph } u. { x | ps } ) = { y | ( y e. { x | ph } \/ y e. { x | ps } ) }
4 df-clab 
 |-  ( y e. { x | ph } <-> [ y / x ] ph )
5 1 sbievw 
 |-  ( [ y / x ] ph <-> ch )
6 4 5 bitri 
 |-  ( y e. { x | ph } <-> ch )
7 df-clab 
 |-  ( y e. { x | ps } <-> [ y / x ] ps )
8 2 sbievw 
 |-  ( [ y / x ] ps <-> th )
9 7 8 bitri 
 |-  ( y e. { x | ps } <-> th )
10 6 9 orbi12i 
 |-  ( ( y e. { x | ph } \/ y e. { x | ps } ) <-> ( ch \/ th ) )
11 10 abbii 
 |-  { y | ( y e. { x | ph } \/ y e. { x | ps } ) } = { y | ( ch \/ th ) }
12 3 11 eqtri 
 |-  ( { x | ph } u. { x | ps } ) = { y | ( ch \/ th ) }