![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rabbiia | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal restricted class abstractions (inference rule). (Contributed by NM, 22-May-1999.) |
Ref | Expression |
---|---|
rabbiia.1 | ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rabbiia | ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbiia.1 | . . . 4 ⊢ (𝑥 ∈ 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | pm5.32i 672 | . . 3 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑥 ∈ 𝐴 ∧ 𝜓)) |
3 | 2 | abbii 2877 | . 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} |
4 | df-rab 3059 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
5 | df-rab 3059 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
6 | 3, 4, 5 | 3eqtr4i 2792 | 1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∈ 𝐴 ∣ 𝜓} |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 ∧ wa 383 = wceq 1632 ∈ wcel 2139 {cab 2746 {crab 3054 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-rab 3059 |
This theorem is referenced by: rabbii 3325 elneldisjOLD 4108 elnelunOLD 4109 fninfp 6605 fndifnfp 6607 nlimon 7217 dfom2 7233 rankval2 8856 ioopos 12463 prmreclem4 15845 acsfn1 16543 acsfn2 16545 logtayl 24626 ftalem3 25021 ppiub 25149 isuvtx 26518 vtxdginducedm1 26670 finsumvtxdg2size 26677 rgrusgrprc 26716 clwwlknclwwlkdif 27121 clwwlknclwwlkdifsOLD 27123 numclwwlkqhash 27557 ubthlem1 28056 xpinpreima 30282 xpinpreima2 30283 eulerpartgbij 30764 topdifinfeq 33527 rabimbieq 34358 rmydioph 38101 rmxdioph 38103 expdiophlem2 38109 expdioph 38110 fsovrfovd 38823 k0004val0 38972 nzss 39036 hashnzfz 39039 fourierdlem90 40934 fourierdlem96 40940 fourierdlem97 40941 fourierdlem98 40942 fourierdlem99 40943 fourierdlem100 40944 fourierdlem109 40953 fourierdlem110 40954 fourierdlem112 40956 fourierdlem113 40957 sssmf 41471 dfodd6 42078 dfeven4 42079 dfeven2 42090 dfodd3 42091 dfeven3 42098 dfodd4 42099 dfodd5 42100 |
Copyright terms: Public domain | W3C validator |