![]() |
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 576 | . 2 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | rabbia2 3411 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1542 ∈ wcel 2107 {crab 3408 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2708 |
This theorem depends on definitions: df-bi 206 df-an 398 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2715 df-cleq 2729 df-rab 3409 |
This theorem is referenced by: rabbii 3414 fninfp 7121 fndifnfp 7123 nlimon 7788 dfom2 7805 rankval2 9755 ioopos 13342 prmreclem4 16792 acsfn1 17542 acsfn2 17544 logtayl 26018 ftalem3 26427 ppiub 26555 isuvtx 28346 vtxdginducedm1 28494 finsumvtxdg2size 28501 rgrusgrprc 28540 clwwlknclwwlkdif 28926 numclwwlkqhash 29322 ubthlem1 29815 xpinpreima 32490 xpinpreima2 32491 eulerpartgbij 32975 topdifinfeq 35824 rabimbieq 36714 rmydioph 41341 rmxdioph 41343 expdiophlem2 41349 expdioph 41350 alephiso3 41838 fsovrfovd 42288 k0004val0 42433 nzss 42604 hashnzfz 42607 fourierdlem90 44444 fourierdlem96 44450 fourierdlem97 44451 fourierdlem98 44452 fourierdlem99 44453 fourierdlem100 44454 fourierdlem109 44463 fourierdlem110 44464 fourierdlem112 44466 fourierdlem113 44467 sssmf 44986 dfodd6 45836 dfeven4 45837 dfeven2 45848 dfodd3 45849 dfeven3 45857 dfodd4 45858 dfodd5 45859 |
Copyright terms: Public domain | W3C validator |