**Description:** Equality theorem for intersection of two classes. (Contributed by NM, 14-Dec-1993) (Proof shortened by SN, 20-Sep-2023)

Ref | Expression | ||
---|---|---|---|

Assertion | ineq1 | ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) |

Step | Hyp | Ref | Expression |
---|---|---|---|

1 | rabeq | ⊢ ( 𝐴 = 𝐵 → { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶 } = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶 } ) | |

2 | dfin5 | ⊢ ( 𝐴 ∩ 𝐶 ) = { 𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐶 } | |

3 | dfin5 | ⊢ ( 𝐵 ∩ 𝐶 ) = { 𝑥 ∈ 𝐵 ∣ 𝑥 ∈ 𝐶 } | |

4 | 1 2 3 | 3eqtr4g | ⊢ ( 𝐴 = 𝐵 → ( 𝐴 ∩ 𝐶 ) = ( 𝐵 ∩ 𝐶 ) ) |