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 3941 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} | |
2 | rabbi2dva.1 | . . 3 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐵 ↔ 𝜓)) | |
3 | 2 | rabbidva 3476 | . 2 ⊢ (𝜑 → {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
4 | 1, 3 | syl5eq 2865 | 1 ⊢ (𝜑 → (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝜓}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 = wceq 1528 ∈ wcel 2105 {crab 3139 ∩ cin 3932 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-rab 3144 df-in 3940 |
This theorem is referenced by: fndmdif 6804 bitsshft 15812 sylow3lem2 18682 leordtvallem1 21746 leordtvallem2 21747 ordtt1 21915 xkoccn 22155 txcnmpt 22160 xkopt 22191 ordthmeolem 22337 qustgphaus 22658 itg2monolem1 24278 lhop1 24538 efopn 25168 dirith 26032 pjvec 29400 pjocvec 29401 neibastop3 33607 diarnN 38145 |
Copyright terms: Public domain | W3C validator |