![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ineq12i | Structured version Visualization version GIF version |
Description: Equality inference for intersection of two classes. (Contributed by NM, 24-Jun-2004.) (Proof shortened by Eric Schmidt, 26-Jan-2007.) |
Ref | Expression |
---|---|
ineq1i.1 | ⊢ 𝐴 = 𝐵 |
ineq12i.2 | ⊢ 𝐶 = 𝐷 |
Ref | Expression |
---|---|
ineq12i | ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ineq1i.1 | . 2 ⊢ 𝐴 = 𝐵 | |
2 | ineq12i.2 | . 2 ⊢ 𝐶 = 𝐷 | |
3 | ineq12 4223 | . 2 ⊢ ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷)) | |
4 | 1, 2, 3 | mp2an 692 | 1 ⊢ (𝐴 ∩ 𝐶) = (𝐵 ∩ 𝐷) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1537 ∩ cin 3962 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-rab 3434 df-in 3970 |
This theorem is referenced by: undir 4293 difundi 4296 difindir 4299 inrab 4322 inrab2 4323 elneldisj 4398 dfif4 4546 dfif5 4547 inxpOLD 5846 resindi 6016 resindir 6017 rnin 6169 inimass 6177 cnvrescnv 6217 predin 6350 funtp 6625 orduniss2 7853 offres 8007 fodomr 9167 fodomfir 9366 epinid0 9638 cnvepnep 9646 wemapwe 9735 cotr3 15014 explecnv 15898 psssdm2 18639 ablfacrp 20101 cnfldfunALT 21397 cnfldfunALTOLD 21410 cnfldfunALTOLDOLD 21411 pjfval2 21747 ofco2 22473 iundisj2 25598 clwwlknondisj 30140 lejdiri 31568 cmbr3i 31629 nonbooli 31680 5oai 31690 3oalem5 31695 mayetes3i 31758 mdexchi 32364 disjpreima 32604 disjxpin 32608 iundisj2f 32610 xppreima 32662 iundisj2fi 32805 xpinpreima 33867 xpinpreima2 33868 ordtcnvNEW 33881 pprodcnveq 35865 dfiota3 35905 bj-inrab 36910 ptrest 37606 ftc1anclem6 37685 xrnres3 38386 br2coss 38420 1cosscnvxrn 38457 refsymrels2 38547 dfeqvrels2 38570 dfeldisj5 38703 dnwech 43037 fgraphopab 43192 onfrALTlem5 44540 onfrALTlem4 44541 onfrALTlem5VD 44883 onfrALTlem4VD 44884 disjxp1 45009 disjinfi 45135 |
Copyright terms: Public domain | W3C validator |