![]() |
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 3722 | . 2 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
2 | df-rab 3059 | . 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝑥 ∈ 𝐵)} | |
3 | 1, 2 | eqtr4i 2785 | 1 ⊢ (𝐴 ∩ 𝐵) = {𝑥 ∈ 𝐴 ∣ 𝑥 ∈ 𝐵} |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 383 = wceq 1632 ∈ wcel 2139 {cab 2746 {crab 3054 ∩ cin 3714 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-an 385 df-ex 1854 df-cleq 2753 df-rab 3059 df-in 3722 |
This theorem is referenced by: nfin 3963 rabbi2dva 3964 dfepfr 5251 epfrc 5252 pmtrmvd 18076 ablfaclem3 18686 mretopd 21098 ptclsg 21620 xkopt 21660 iscmet3 23291 xrlimcnp 24894 ppiub 25128 xppreima 29758 fpwrelmapffs 29818 orvcelval 30839 sstotbnd2 33886 glbconN 35166 2polssN 35704 rfovcnvf1od 38800 fsovcnvlem 38809 ntrneifv3 38882 ntrneifv4 38885 clsneifv3 38910 clsneifv4 38911 neicvgfv 38921 |
Copyright terms: Public domain | W3C validator |