Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > inrab | Structured version Visualization version GIF version |
Description: Intersection of two restricted class abstractions. (Contributed by NM, 1-Sep-2006.) |
Ref | Expression |
---|---|
inrab | ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-rab 3147 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | df-rab 3147 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
3 | 1, 2 | ineq12i 4187 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
4 | df-rab 3147 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} | |
5 | inab 4271 | . . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))} | |
6 | anandi 674 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) | |
7 | 6 | abbii 2886 | . . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))} |
8 | 5, 7 | eqtr4i 2847 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} |
9 | 4, 8 | eqtr4i 2847 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
10 | 3, 9 | eqtr4i 2847 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 398 = wceq 1537 ∈ wcel 2114 {cab 2799 {crab 3142 ∩ cin 3935 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2793 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-tru 1540 df-ex 1781 df-nf 1785 df-sb 2070 df-clab 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-rab 3147 df-v 3496 df-in 3943 |
This theorem is referenced by: rabnc 4341 ixxin 12756 hashbclem 13811 phiprmpw 16113 submacs 17991 ablfacrp 19188 dfrhm2 19469 ordtbaslem 21796 ordtbas2 21799 ordtopn3 21804 ordtcld3 21807 ordthauslem 21991 pthaus 22246 xkohaus 22261 tsmsfbas 22736 minveclem3b 24031 shftmbl 24139 mumul 25758 ppiub 25780 lgsquadlem2 25957 umgrislfupgrlem 26907 numedglnl 26929 clwwlknondisj 27890 frcond3 28048 numclwwlk3lem2 28163 xppreima 30394 xpinpreima 31149 xpinpreima2 31150 measvuni 31473 subfacp1lem6 32432 satfv1 32610 cnambfre 34955 itg2addnclem2 34959 ftc1anclem6 34987 refsymrels2 35816 dfeqvrels2 35838 refrelsredund4 35882 anrabdioph 39397 undisjrab 40658 smfaddlem2 43060 smfmullem4 43089 |
Copyright terms: Public domain | W3C validator |