# Metamath Proof Explorer

## Theorem elunant

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 ${⊢}\left({C}\in \left({A}\cup {B}\right)\to {\phi }\right)↔\left(\left({C}\in {A}\to {\phi }\right)\wedge \left({C}\in {B}\to {\phi }\right)\right)$

### Proof

Step Hyp Ref Expression
1 elun ${⊢}{C}\in \left({A}\cup {B}\right)↔\left({C}\in {A}\vee {C}\in {B}\right)$
2 1 imbi1i ${⊢}\left({C}\in \left({A}\cup {B}\right)\to {\phi }\right)↔\left(\left({C}\in {A}\vee {C}\in {B}\right)\to {\phi }\right)$
3 jaob ${⊢}\left(\left({C}\in {A}\vee {C}\in {B}\right)\to {\phi }\right)↔\left(\left({C}\in {A}\to {\phi }\right)\wedge \left({C}\in {B}\to {\phi }\right)\right)$
4 2 3 bitri ${⊢}\left({C}\in \left({A}\cup {B}\right)\to {\phi }\right)↔\left(\left({C}\in {A}\to {\phi }\right)\wedge \left({C}\in {B}\to {\phi }\right)\right)$