![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > dfin5 | Structured version Visualization version GIF version |
Description: Alternate definition for the intersection of two classes. (Contributed by NM, 6-Jul-2005.) |
Ref | Expression |
---|---|
dfin5 | ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-in 3970 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | df-rab 3434 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 1, 2 | eqtr4i 2766 | 1 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 395 = wceq 1537 ∈ wcel 2106 {cab 2712 {crab 3433 ∩ cin 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-rab 3434 df-in 3970 |
This theorem is referenced by: incom 4217 ineq1 4221 nfinOLD 4233 rabbi2dva 4234 dfss7 4257 dfepfr 5673 epfrc 5674 pmtrmvd 19489 ablfaclem3 20122 mretopd 23116 ptclsg 23639 xkopt 23679 iscmet3 25341 xrlimcnp 27026 ppiub 27263 xppreima 32662 fpwrelmapffs 32752 orvcelval 34450 sstotbnd2 37761 glbconN 39359 glbconNOLD 39360 2polssN 39898 rfovcnvf1od 43994 fsovcnvlem 44003 ntrneifv3 44072 ntrneifv4 44075 clsneifv3 44100 clsneifv4 44101 neicvgfv 44111 inpw 48667 |
Copyright terms: Public domain | W3C validator |