Description: Two classes related by the indexed union over operator values where the index varies the second input is equivalent to the existence of at least one index such that the two classes are related by that operator value. (Contributed by RP, 1-Jun-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | briunov2.def | ||
Assertion | briunov2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | briunov2.def | ||
2 | 1 | eliunov2 | |
3 | df-br | ||
4 | df-br | ||
5 | 4 | rexbii | |
6 | 2 3 5 | 3bitr4g |