![]() |
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 413 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
4 | 3 | ssrdv 3948 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
5 | 1, 4 | eqssd 3959 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1541 ∈ wcel 2106 ⊆ wss 3908 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-v 3445 df-in 3915 df-ss 3925 |
This theorem is referenced by: wfrlem10OLD 8260 ordtypelem9 9458 ordtypelem10 9459 oismo 9472 prlem934 10965 phimullem 16643 prmreclem5 16784 psssdm2 18462 sylow3lem3 19402 ablfacrp 19836 isdrng2 20183 fidomndrng 20763 pjfo 21106 obs2ss 21120 frlmsslsp 21187 mplbas2 21427 restfpw 22514 2ndcsep 22794 ptclsg 22950 trfg 23226 restutopopn 23574 unirnblps 23756 unirnbl 23757 clsocv 24598 rrxbasefi 24758 pjth 24787 opnmbllem 24949 dvidlem 25263 dvaddf 25290 dvmulf 25291 dvcof 25296 dvcj 25298 dvrec 25303 dvcnv 25325 dvcnvre 25367 ftc1cn 25391 ulmdv 25746 pserdv 25772 ppisval2 26438 nbupgruvtxres 28241 dimkerim 32199 fedgmul 32203 reff 32289 dya2iocuni 32752 cvmsss2 33737 opnmbllem0 36081 ftc1cnnc 36117 lkrlsp 37531 cdleme50rnlem 38974 hdmaprnN 40294 hgmaprnN 40331 qsalrel 40629 kercvrlsm 41348 pwssplit4 41354 hbtlem5 41393 restuni3 43270 disjf1o 43346 unirnmapsn 43371 iunmapsn 43374 icoiccdif 43694 iccdificc 43709 lptioo2 43804 lptioo1 43805 qndenserrn 44472 intsaluni 44502 iundjiun 44633 meadjiunlem 44638 meaiininclem 44659 iunhoiioo 44849 |
Copyright terms: Public domain | W3C validator |