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 3073 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} | |
2 | df-rab 3073 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜓} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)} | |
3 | 1, 2 | ineq12i 4144 | . 2 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
4 | df-rab 3073 | . . 3 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} | |
5 | inab 4233 | . . . 4 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))} | |
6 | anandi 673 | . . . . 5 ⊢ ((𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))) | |
7 | 6 | abbii 2808 | . . . 4 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} = {𝑥 ∣ ((𝑥 ∈ 𝐴 ∧ 𝜑) ∧ (𝑥 ∈ 𝐴 ∧ 𝜓))} |
8 | 5, 7 | eqtr4i 2769 | . . 3 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ (𝜑 ∧ 𝜓))} |
9 | 4, 8 | eqtr4i 2769 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} = ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} ∩ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜓)}) |
10 | 3, 9 | eqtr4i 2769 | 1 ⊢ ({𝑥 ∈ 𝐴 ∣ 𝜑} ∩ {𝑥 ∈ 𝐴 ∣ 𝜓}) = {𝑥 ∈ 𝐴 ∣ (𝜑 ∧ 𝜓)} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1539 ∈ wcel 2106 {cab 2715 {crab 3068 ∩ cin 3886 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1542 df-ex 1783 df-sb 2068 df-clab 2716 df-cleq 2730 df-clel 2816 df-rab 3073 df-v 3434 df-in 3894 |
This theorem is referenced by: rabnc 4321 ixxin 13096 hashbclem 14164 phiprmpw 16477 submacs 18465 ablfacrp 19669 dfrhm2 19961 ordtbaslem 22339 ordtbas2 22342 ordtopn3 22347 ordtcld3 22350 ordthauslem 22534 pthaus 22789 xkohaus 22804 tsmsfbas 23279 minveclem3b 24592 shftmbl 24702 mumul 26330 ppiub 26352 lgsquadlem2 26529 umgrislfupgrlem 27492 numedglnl 27514 clwwlknondisj 28475 frcond3 28633 numclwwlk3lem2 28748 xppreima 30983 xpinpreima 31856 xpinpreima2 31857 measvuni 32182 subfacp1lem6 33147 satfv1 33325 cnambfre 35825 itg2addnclem2 35829 ftc1anclem6 35855 refsymrels2 36679 dfeqvrels2 36701 refrelsredund4 36745 anrabdioph 40602 undisjrab 41924 smfaddlem2 44299 smfmullem4 44328 |
Copyright terms: Public domain | W3C validator |