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 | ⊢ ( ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ( ( 𝐶 ∈ 𝐴 → 𝜑 ) ∧ ( 𝐶 ∈ 𝐵 → 𝜑 ) ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elun | ⊢ ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵 ) ) | |
2 | 1 | imbi1i | ⊢ ( ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵 ) → 𝜑 ) ) |
3 | jaob | ⊢ ( ( ( 𝐶 ∈ 𝐴 ∨ 𝐶 ∈ 𝐵 ) → 𝜑 ) ↔ ( ( 𝐶 ∈ 𝐴 → 𝜑 ) ∧ ( 𝐶 ∈ 𝐵 → 𝜑 ) ) ) | |
4 | 2 3 | bitri | ⊢ ( ( 𝐶 ∈ ( 𝐴 ∪ 𝐵 ) → 𝜑 ) ↔ ( ( 𝐶 ∈ 𝐴 → 𝜑 ) ∧ ( 𝐶 ∈ 𝐵 → 𝜑 ) ) ) |