![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rabbidv | GIF version |
Description: Equivalent wff's yield equal restricted class abstractions (deduction form). (Contributed by NM, 10-Feb-1995.) |
Ref | Expression |
---|---|
rabbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
rabbidv | ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rabbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | adantr 276 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
3 | 2 | rabbidva 2740 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1364 ∈ wcel 2160 {crab 2472 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-ral 2473 df-rab 2477 |
This theorem is referenced by: rabeqbidv 2747 difeq2 3262 seex 4353 mptiniseg 5141 supeq1 7015 supeq2 7018 supeq3 7019 cardcl 7210 isnumi 7211 cardval3ex 7214 carden2bex 7218 genpdflem 7536 genipv 7538 genpelxp 7540 addcomprg 7607 mulcomprg 7609 uzval 9560 ixxval 9926 fzval 10040 hashinfom 10790 hashennn 10792 shftfn 10865 gcdval 11992 lcmval 12095 isprm 12141 odzval 12273 pceulem 12326 pceu 12327 pcval 12328 pczpre 12329 pcdiv 12334 lspval 13706 istopon 13973 toponsspwpwg 13982 clsval 14071 neival 14103 cnpval 14158 blvalps 14348 blval 14349 limccl 14588 ellimc3apf 14589 eldvap 14611 |
Copyright terms: Public domain | W3C validator |