![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > inteq | Structured version Visualization version GIF version |
Description: Equality law for intersection. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
inteq | ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | raleq 3308 | . . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)) | |
2 | 1 | abbidv 2807 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}) |
3 | dfint2 4908 | . 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | |
4 | dfint2 4908 | . 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦} | |
5 | 2, 3, 4 | 3eqtr4g 2803 | 1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1542 {cab 2715 ∀wral 3063 ∩ cint 4906 |
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 1914 ax-6 1972 ax-7 2012 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-ral 3064 df-int 4907 |
This theorem is referenced by: inteqi 4910 inteqd 4911 unissint 4932 uniintsn 4947 rint0 4950 intex 5293 intnex 5294 elreldm 5887 elxp5 7851 1stval2 7929 oev2 8437 fundmen 8909 xpsnen 8933 fiint 9202 elfir 9285 inelfi 9288 fiin 9292 cardmin2 9869 isfin2-2 10189 incexclem 15657 mreintcl 17411 ismred2 17419 fiinopn 22178 cmpfii 22688 ptbasfi 22860 fbssint 23117 shintcl 30077 chintcl 30079 zarcmplem 32242 inelpisys 32533 rankeq1o 34687 bj-0int 35503 bj-ismoored 35509 bj-snmoore 35515 bj-prmoore 35517 neificl 36143 heibor1lem 36199 elrfi 40919 elrfirn 40920 |
Copyright terms: Public domain | W3C validator |