![]() |
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 274 | . 2 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝜓 ↔ 𝜒)) |
3 | 2 | rabbidva 2677 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1332 ∈ wcel 1481 {crab 2421 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1483 ax-11 1485 ax-4 1488 ax-17 1507 ax-i9 1511 ax-ial 1515 ax-i5r 1516 ax-ext 2122 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1737 df-clab 2127 df-cleq 2133 df-ral 2422 df-rab 2426 |
This theorem is referenced by: rabeqbidv 2684 difeq2 3193 seex 4265 mptiniseg 5041 supeq1 6881 supeq2 6884 supeq3 6885 cardcl 7054 isnumi 7055 cardval3ex 7058 carden2bex 7062 genpdflem 7339 genipv 7341 genpelxp 7343 addcomprg 7410 mulcomprg 7412 uzval 9352 ixxval 9709 fzval 9823 hashinfom 10556 hashennn 10558 shftfn 10628 gcdval 11684 lcmval 11780 isprm 11826 istopon 12219 toponsspwpwg 12228 clsval 12319 neival 12351 cnpval 12406 blvalps 12596 blval 12597 limccl 12836 ellimc3apf 12837 eldvap 12859 |
Copyright terms: Public domain | W3C validator |