Description: A statement is true for every element of the union of a pair of classes if and only if it is true for every element of the first class and for every element of the second class. (Contributed by BTernaryTau, 27-Sep-2023)
Ref | Expression | ||
---|---|---|---|
Assertion | elunant | |- ( ( C e. ( A u. B ) -> ph ) <-> ( ( C e. A -> ph ) /\ ( C e. B -> ph ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elun | |- ( C e. ( A u. B ) <-> ( C e. A \/ C e. B ) ) |
|
2 | 1 | imbi1i | |- ( ( C e. ( A u. B ) -> ph ) <-> ( ( C e. A \/ C e. B ) -> ph ) ) |
3 | jaob | |- ( ( ( C e. A \/ C e. B ) -> ph ) <-> ( ( C e. A -> ph ) /\ ( C e. B -> ph ) ) ) |
|
4 | 2 3 | bitri | |- ( ( C e. ( A u. B ) -> ph ) <-> ( ( C e. A -> ph ) /\ ( C e. B -> ph ) ) ) |