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 3403 | . . 3 ⊢ (𝐴 = 𝐵 → (∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 ↔ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦)) | |
2 | 1 | abbidv 2882 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦}) |
3 | dfint2 4869 | . 2 ⊢ ∩ 𝐴 = {𝑥 ∣ ∀𝑦 ∈ 𝐴 𝑥 ∈ 𝑦} | |
4 | dfint2 4869 | . 2 ⊢ ∩ 𝐵 = {𝑥 ∣ ∀𝑦 ∈ 𝐵 𝑥 ∈ 𝑦} | |
5 | 2, 3, 4 | 3eqtr4g 2878 | 1 ⊢ (𝐴 = 𝐵 → ∩ 𝐴 = ∩ 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1528 {cab 2796 ∀wral 3135 ∩ cint 4867 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-ex 1772 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-ral 3140 df-int 4868 |
This theorem is referenced by: inteqi 4871 inteqd 4872 unissint 4891 uniintsn 4904 rint0 4907 intex 5231 intnex 5232 elreldm 5798 elxp5 7617 1stval2 7695 oev2 8137 fundmen 8571 xpsnen 8589 fiint 8783 elfir 8867 inelfi 8870 fiin 8874 cardmin2 9415 isfin2-2 9729 incexclem 15179 mreintcl 16854 ismred2 16862 fiinopn 21437 cmpfii 21945 ptbasfi 22117 fbssint 22374 shintcl 29034 chintcl 29036 inelpisys 31312 rankeq1o 33529 bj-0int 34287 bj-ismoored 34293 bj-snmoore 34299 neificl 34909 heibor1lem 34968 elrfi 39169 elrfirn 39170 |
Copyright terms: Public domain | W3C validator |