Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > rabbi2dva | Structured version Visualization version GIF version |
Description: Deduction from a wff to a restricted class abstraction. (Contributed by NM, 14-Jan-2014.) |
Ref | Expression |
---|---|
rabbi2dva.1 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) |
Ref | Expression |
---|---|
rabbi2dva | ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfin5 3548 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | |
2 | rabbi2dva.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) | |
3 | 2 | rabbidva 3163 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
4 | 1, 3 | syl5eq 2656 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 = wceq 1475 ∈ wcel 1977 {crab 2900 ∩ cin 3539 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-ral 2901 df-rab 2905 df-in 3547 |
This theorem is referenced by: fndmdif 6229 bitsshft 15035 sylow3lem2 17866 leordtvallem1 20824 leordtvallem2 20825 ordtt1 20993 xkoccn 21232 txcnmpt 21237 xkopt 21268 ordthmeolem 21414 qustgphaus 21736 itg2monolem1 23323 lhop1 23581 efopn 24204 dirith 25018 pjvec 27939 pjocvec 27940 neibastop3 31527 diarnN 35436 |
Copyright terms: Public domain | W3C validator |