|   | 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 3322 | . . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)) | |
| 2 | 1 | abbidv 2807 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}) | 
| 3 | dfint2 4947 | . 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | |
| 4 | dfint2 4947 | . 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦} | |
| 5 | 2, 3, 4 | 3eqtr4g 2801 | 1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 = wceq 1539 {cab 2713 ∀wral 3060 ∩ cint 4945 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-ral 3061 df-rex 3070 df-int 4946 | 
| This theorem is referenced by: inteqi 4949 inteqd 4950 unissint 4971 uniintsn 4984 rint0 4987 intex 5343 intnex 5344 elreldm 5945 elxp5 7946 1stval2 8032 oev2 8562 fundmen 9072 xpsnen 9096 fiint 9367 fiintOLD 9368 elfir 9456 inelfi 9459 fiin 9463 cardmin2 10040 isfin2-2 10360 incexclem 15873 mreintcl 17639 ismred2 17647 fiinopn 22908 cmpfii 23418 ptbasfi 23590 fbssint 23847 shintcl 31350 chintcl 31352 zarcmplem 33881 inelpisys 34156 rankeq1o 36173 bj-0int 37103 bj-ismoored 37109 bj-snmoore 37115 bj-prmoore 37117 neificl 37761 heibor1lem 37817 elrfi 42710 elrfirn 42711 | 
| Copyright terms: Public domain | W3C validator |