Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > eqssd | GIF version |
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.) |
Ref | Expression |
---|---|
eqssd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
eqssd.2 | ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
Ref | Expression |
---|---|
eqssd | ⊢ (𝜑 → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqssd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | eqssd.2 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | |
3 | eqss 3152 | . 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴)) | |
4 | 1, 2, 3 | sylanbrc 414 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff set class |
Syntax hints: → wi 4 = wceq 1342 ⊆ wss 3111 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-11 1493 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-in 3117 df-ss 3124 |
This theorem is referenced by: eqrd 3155 eqelssd 3156 unissel 3812 intmin 3838 int0el 3848 pwntru 4172 exmidundif 4179 exmidundifim 4180 dmcosseq 4869 relfld 5126 imadif 5262 imain 5264 fimacnv 5608 fo2ndf 6186 tposeq 6206 tfrlemibfn 6287 tfrlemi14d 6292 tfr1onlembfn 6303 tfri1dALT 6310 tfrcllembfn 6316 dcdifsnid 6463 fisbth 6840 en2eqpr 6864 exmidpw 6865 exmidpweq 6866 undifdcss 6879 nnnninfeq2 7084 en2other2 7143 exmidontriimlem3 7170 addnqpr 7493 mulnqpr 7509 distrprg 7520 ltexpri 7545 addcanprg 7548 recexprlemex 7569 aptipr 7573 cauappcvgprlemladd 7590 fzopth 9986 fzosplit 10102 fzouzsplit 10104 frecuzrdgtcl 10337 frecuzrdgdomlem 10342 zsupssdc 11872 phimullem 12136 structcnvcnv 12353 eltg4i 12602 unitg 12609 tgtop 12615 tgidm 12621 basgen 12627 2basgeng 12629 epttop 12637 ntrin 12671 isopn3 12672 neiuni 12708 tgrest 12716 resttopon 12718 rest0 12726 txdis 12824 hmeontr 12860 xmettx 13057 findset 13668 pwtrufal 13718 pwf1oexmid 13720 |
Copyright terms: Public domain | W3C validator |