| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > eqrd | Structured version Visualization version GIF version | ||
| Description: Deduce equality of classes from equivalence of membership. (Contributed by Thierry Arnoux, 21-Mar-2017.) (Proof shortened by BJ, 1-Dec-2021.) |
| Ref | Expression |
|---|---|
| eqrd.0 | ⊢ Ⅎ𝑥𝜑 |
| eqrd.1 | ⊢ Ⅎ𝑥𝐴 |
| eqrd.2 | ⊢ Ⅎ𝑥𝐵 |
| eqrd.3 | ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| Ref | Expression |
|---|---|
| eqrd | ⊢ (𝜑 → 𝐴 = 𝐵) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eqrd.0 | . . 3 ⊢ Ⅎ𝑥𝜑 | |
| 2 | eqrd.3 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) | |
| 3 | 1, 2 | alrimi 2213 | . 2 ⊢ (𝜑 → ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| 4 | eqrd.1 | . . 3 ⊢ Ⅎ𝑥𝐴 | |
| 5 | eqrd.2 | . . 3 ⊢ Ⅎ𝑥𝐵 | |
| 6 | 4, 5 | cleqf 2934 | . 2 ⊢ (𝐴 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ 𝑥 ∈ 𝐵)) |
| 7 | 3, 6 | sylibr 234 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∀wal 1538 = wceq 1540 Ⅎwnf 1783 ∈ wcel 2108 Ⅎwnfc 2890 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-11 2157 ax-12 2177 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-tru 1543 df-ex 1780 df-nf 1784 df-cleq 2729 df-clel 2816 df-nfc 2892 |
| This theorem is referenced by: eqri 4004 eqrrabd 4086 sniota 6552 fimarab 6983 dissnlocfin 23537 imasnopn 23698 imasncld 23699 imasncls 23700 blval2 24575 ofpreima 32675 algextdeglem6 33763 constrfin 33787 zarcls 33873 ordtconnlem1 33923 qqhval2 33983 reprdifc 34642 topdifinfindis 37347 icorempo 37352 isbasisrelowllem1 37356 isbasisrelowllem2 37357 sticksstones11 42157 areaquad 43228 rfcnpre1 45024 rfcnpre2 45036 preimagelt 46714 preimalegt 46715 |
| Copyright terms: Public domain | W3C validator |