![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > eqelssd | Structured version Visualization version GIF version |
Description: Equality deduction from subclass relationship and membership. (Contributed by AV, 21-Aug-2022.) |
Ref | Expression |
---|---|
eqelssd.1 | ⊢ (𝜑 → 𝐴 ⊆ 𝐵) |
eqelssd.2 | ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) |
Ref | Expression |
---|---|
eqelssd | ⊢ (𝜑 → 𝐴 = 𝐵) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqelssd.1 | . 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵) | |
2 | eqelssd.2 | . . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → 𝑥 ∈ 𝐴) | |
3 | 2 | ex 412 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
4 | 3 | ssrdv 4001 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
5 | 1, 4 | eqssd 4013 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2106 ⊆ wss 3963 |
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-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1777 df-cleq 2727 df-ss 3980 |
This theorem is referenced by: wfrlem10OLD 8357 ordtypelem9 9564 ordtypelem10 9565 oismo 9578 prlem934 11071 phimullem 16813 prmreclem5 16954 psssdm2 18639 sylow3lem3 19662 ablfacrp 20101 isdrng2 20760 fidomndrng 20791 imadrhmcl 20815 pjfo 21753 obs2ss 21767 frlmsslsp 21834 mplbas2 22078 restfpw 23203 2ndcsep 23483 ptclsg 23639 trfg 23915 restutopopn 24263 unirnblps 24445 unirnbl 24446 clsocv 25298 rrxbasefi 25458 pjth 25487 opnmbllem 25650 dvidlem 25965 dvaddf 25994 dvmulf 25995 dvcof 26001 dvcj 26003 dvrec 26008 dvcnv 26030 dvcnvre 26073 ftc1cn 26099 ulmdv 26461 pserdv 26488 ppisval2 27163 noseqrdgfn 28327 nbupgruvtxres 29439 ply1degltdimlem 33650 dimkerim 33655 fedgmul 33659 assafld 33665 reff 33800 dya2iocuni 34265 cvmsss2 35259 opnmbllem0 37643 ftc1cnnc 37679 lkrlsp 39084 cdleme50rnlem 40527 hdmaprnN 41847 hgmaprnN 41884 qsalrel 42260 kercvrlsm 43072 pwssplit4 43078 hbtlem5 43117 restuni3 45058 disjf1o 45134 unirnmapsn 45157 iunmapsn 45160 icoiccdif 45477 iccdificc 45492 lptioo2 45587 lptioo1 45588 qndenserrn 46255 intsaluni 46285 iundjiun 46416 meadjiunlem 46421 meaiininclem 46442 iunhoiioo 46632 |
Copyright terms: Public domain | W3C validator |