| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eleq12 | Structured version Visualization version GIF version | ||
| Description: Equality implies equivalence of membership. (Contributed by NM, 31-May-1999.) |
| Ref | Expression |
|---|---|
| eleq12 | ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eleq1 2853 | . 2 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐶)) | |
| 2 | eleq2 2854 | . 2 ⊢ (𝐶 = 𝐷 → (𝐵 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) | |
| 3 | 1, 2 | sylan9bb 519 | 1 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∈ 𝐶 ↔ 𝐵 ∈ 𝐷)) |
| Colors of variables: wff setvar class |
| This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 |
| This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-ext 2737 |
| This proof depends on definitions: df-bi 210 df-an 402 df-ex 1813 df-cleq 2757 df-clel 2840 |
| This theorem is used by: rru 3744 trel 5228 epelg 5564 preleqg 9591 preleqALT 9593 oemapval 9659 cantnf 9669 wemapwe 9673 nnsdomel 9992 cldval 23230 isufil 24111 taylthlem2 26588 umgr2v2enb1 29934 issiga 34566 bj-epelg 37761 rdgssun 38081 matunitlindf 38326 wepwsolem 43827 aomclem8 43846 grumnud 45054 nelbr 48069 |
| Copyright terms: Public domain | W3C validator |