![]() |
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 411 | . . 3 ⊢ (𝜑 → (𝑥 ∈ 𝐵 → 𝑥 ∈ 𝐴)) |
4 | 3 | ssrdv 3984 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
5 | 1, 4 | eqssd 3996 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ⊆ wss 3946 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1775 df-cleq 2718 df-ss 3963 |
This theorem is referenced by: wfrlem10OLD 8340 ordtypelem9 9562 ordtypelem10 9563 oismo 9576 prlem934 11067 phimullem 16776 prmreclem5 16917 psssdm2 18601 sylow3lem3 19623 ablfacrp 20062 isdrng2 20717 fidomndrng 20748 imadrhmcl 20772 pjfo 21709 obs2ss 21723 frlmsslsp 21790 mplbas2 22045 restfpw 23171 2ndcsep 23451 ptclsg 23607 trfg 23883 restutopopn 24231 unirnblps 24413 unirnbl 24414 clsocv 25266 rrxbasefi 25426 pjth 25455 opnmbllem 25618 dvidlem 25932 dvaddf 25961 dvmulf 25962 dvcof 25968 dvcj 25970 dvrec 25975 dvcnv 25997 dvcnvre 26040 ftc1cn 26066 ulmdv 26429 pserdv 26456 ppisval2 27130 noseqrdgfn 28277 nbupgruvtxres 29340 ply1degltdimlem 33523 dimkerim 33528 fedgmul 33532 reff 33667 dya2iocuni 34130 cvmsss2 35115 opnmbllem0 37370 ftc1cnnc 37406 lkrlsp 38813 cdleme50rnlem 40256 hdmaprnN 41576 hgmaprnN 41613 qsalrel 41986 kercvrlsm 42781 pwssplit4 42787 hbtlem5 42826 restuni3 44756 disjf1o 44834 unirnmapsn 44857 iunmapsn 44860 icoiccdif 45178 iccdificc 45193 lptioo2 45288 lptioo1 45289 qndenserrn 45956 intsaluni 45986 iundjiun 46117 meadjiunlem 46122 meaiininclem 46143 iunhoiioo 46333 |
Copyright terms: Public domain | W3C validator |