![]() |
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 3951 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | df-rab 3432 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 1, 2 | eqtr4i 2762 | 1 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 396 = wceq 1541 ∈ wcel 2106 {cab 2708 {crab 3431 ∩ cin 3943 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-ex 1782 df-cleq 2723 df-rab 3432 df-in 3951 |
This theorem is referenced by: incom 4197 ineq1 4201 nfin 4212 rabbi2dva 4213 dfss7 4236 dfepfr 5654 epfrc 5655 pmtrmvd 19288 ablfaclem3 19916 mretopd 22525 ptclsg 23048 xkopt 23088 iscmet3 24739 xrlimcnp 26400 ppiub 26634 xppreima 31740 fpwrelmapffs 31830 orvcelval 33298 sstotbnd2 36447 glbconN 38052 glbconNOLD 38053 2polssN 38591 rfovcnvf1od 42526 fsovcnvlem 42535 ntrneifv3 42604 ntrneifv4 42607 clsneifv3 42632 clsneifv4 42633 neicvgfv 42643 inpw 47151 |
Copyright terms: Public domain | W3C validator |