| 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 3989 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| 5 | 1, 4 | eqssd 4001 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∧ wa 395 = wceq 1540 ∈ wcel 2108 ⊆ wss 3951 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-cleq 2729 df-ss 3968 |
| This theorem is referenced by: wfrlem10OLD 8358 ordtypelem9 9566 ordtypelem10 9567 oismo 9580 prlem934 11073 phimullem 16816 prmreclem5 16958 psssdm2 18626 sylow3lem3 19647 ablfacrp 20086 isdrng2 20743 fidomndrng 20774 imadrhmcl 20798 pjfo 21735 obs2ss 21749 frlmsslsp 21816 mplbas2 22060 restfpw 23187 2ndcsep 23467 ptclsg 23623 trfg 23899 restutopopn 24247 unirnblps 24429 unirnbl 24430 clsocv 25284 rrxbasefi 25444 pjth 25473 opnmbllem 25636 dvidlem 25950 dvaddf 25979 dvmulf 25980 dvcof 25986 dvcj 25988 dvrec 25993 dvcnv 26015 dvcnvre 26058 ftc1cn 26084 ulmdv 26446 pserdv 26473 ppisval2 27148 noseqrdgfn 28312 nbupgruvtxres 29424 ply1degltdimlem 33673 dimkerim 33678 fedgmul 33682 assafld 33688 reff 33838 dya2iocuni 34285 cvmsss2 35279 opnmbllem0 37663 ftc1cnnc 37699 lkrlsp 39103 cdleme50rnlem 40546 hdmaprnN 41866 hgmaprnN 41903 qsalrel 42281 kercvrlsm 43095 pwssplit4 43101 hbtlem5 43140 restuni3 45123 disjf1o 45196 unirnmapsn 45219 iunmapsn 45222 icoiccdif 45537 iccdificc 45552 lptioo2 45646 lptioo1 45647 qndenserrn 46314 intsaluni 46344 iundjiun 46475 meadjiunlem 46480 meaiininclem 46501 iunhoiioo 46691 |
| Copyright terms: Public domain | W3C validator |