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 2648 | 1 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∈ 𝐴 ∣ 𝜒}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 = wceq 1316 ∈ wcel 1465 {crab 2397 |
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 1408 ax-7 1409 ax-gen 1410 ax-ie1 1454 ax-ie2 1455 ax-8 1467 ax-11 1469 ax-4 1472 ax-17 1491 ax-i9 1495 ax-ial 1499 ax-i5r 1500 ax-ext 2099 |
This theorem depends on definitions: df-bi 116 df-tru 1319 df-nf 1422 df-sb 1721 df-clab 2104 df-cleq 2110 df-ral 2398 df-rab 2402 |
This theorem is referenced by: rabeqbidv 2655 difeq2 3158 seex 4227 mptiniseg 5003 supeq1 6841 supeq2 6844 supeq3 6845 cardcl 7005 isnumi 7006 cardval3ex 7009 carden2bex 7013 genpdflem 7283 genipv 7285 genpelxp 7287 addcomprg 7354 mulcomprg 7356 uzval 9296 ixxval 9647 fzval 9760 hashinfom 10492 hashennn 10494 shftfn 10564 gcdval 11575 lcmval 11671 isprm 11717 istopon 12107 toponsspwpwg 12116 clsval 12207 neival 12239 cnpval 12294 blvalps 12484 blval 12485 limccl 12724 ellimc3apf 12725 eldvap 12747 |
Copyright terms: Public domain | W3C validator |