| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rabbiia | Structured version Visualization version GIF version | ||
| Description: Equivalent formulas yield equal restricted class abstractions (inference form). (Contributed by NM, 22-May-1999.) (Proof shortened by Wolf Lammen, 12-Jan-2025.) |
| Ref | Expression |
|---|---|
| rabbiia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rabbiia | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rabbiia.1 | . . 3 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) | |
| 2 | 1 | pm5.32i 574 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
| 3 | 2 | rabbia2 3404 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1542 ∈ wcel 2114 {crab 3401 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-9 2124 ax-ext 2709 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1545 df-ex 1782 df-sb 2069 df-clab 2716 df-cleq 2729 df-rab 3402 |
| This theorem is referenced by: rabbii 3406 fninfp 7132 fndifnfp 7134 nlimon 7805 dfom2 7822 rankval2 9744 ioopos 13354 prmreclem4 16861 acsfn1 17598 acsfn2 17600 logtayl 26642 ftalem3 27058 ppiub 27188 isuvtx 29486 vtxdginducedm1 29635 finsumvtxdg2size 29642 rgrusgrprc 29681 clwwlknclwwlkdif 30072 numclwwlkqhash 30468 ubthlem1 30964 psrbasfsupp 33711 xpinpreima 34090 xpinpreima2 34091 eulerpartgbij 34556 rankval2b 35282 fineqvnttrclse 35308 topdifinfeq 37632 rabimbieq 38533 resuppsinopn 42762 rmydioph 43400 rmxdioph 43402 expdiophlem2 43408 expdioph 43409 alephiso3 43944 fsovrfovd 44394 k0004val0 44539 nzss 44702 hashnzfz 44705 fourierdlem90 46583 fourierdlem96 46589 fourierdlem97 46590 fourierdlem98 46591 fourierdlem99 46592 fourierdlem100 46593 fourierdlem109 46602 fourierdlem110 46603 fourierdlem112 46605 fourierdlem113 46606 sssmf 47125 dfodd6 48026 dfeven4 48027 dfeven2 48038 dfodd3 48039 dfeven3 48047 dfodd4 48048 dfodd5 48049 |
| Copyright terms: Public domain | W3C validator |