![]() |
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 3897 | . 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
5 | 1, 4 | eqssd 3908 | 1 ⊢ (𝜑 → 𝐴 = 𝐵) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 = wceq 1522 ∈ wcel 2080 ⊆ wss 3861 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1778 ax-4 1792 ax-5 1889 ax-6 1948 ax-7 1993 ax-8 2082 ax-9 2090 ax-10 2111 ax-11 2125 ax-12 2140 ax-ext 2768 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-tru 1525 df-ex 1763 df-nf 1767 df-sb 2042 df-clab 2775 df-cleq 2787 df-clel 2862 df-in 3868 df-ss 3876 |
This theorem is referenced by: wfrlem10 7819 ordtypelem9 8839 ordtypelem10 8840 oismo 8853 prlem934 10304 phimullem 15945 prmreclem5 16085 psssdm2 17654 sylow3lem3 18484 ablfacrp 18905 isdrng2 19202 fidomndrng 19769 mplbas2 19938 pjfo 20541 obs2ss 20555 frlmsslsp 20622 restfpw 21471 2ndcsep 21751 ptclsg 21907 trfg 22183 restutopopn 22530 unirnblps 22712 unirnbl 22713 clsocv 23536 rrxbasefi 23696 pjth 23725 opnmbllem 23885 dvidlem 24196 dvaddf 24222 dvmulf 24223 dvcof 24228 dvcj 24230 dvrec 24235 dvcnv 24257 dvcnvre 24299 ftc1cn 24323 ulmdv 24674 pserdv 24700 ppisval2 25364 nbupgruvtxres 26872 dimkerim 30619 fedgmul 30623 reff 30712 dya2iocuni 31150 cvmsss2 32123 opnmbllem0 34472 ftc1cnnc 34510 lkrlsp 35782 cdleme50rnlem 37224 hdmaprnN 38544 hgmaprnN 38581 kercvrlsm 39181 pwssplit4 39187 hbtlem5 39226 restuni3 40937 disjf1o 41005 unirnmapsn 41030 iunmapsn 41033 icoiccdif 41355 iccdificc 41370 lptioo2 41467 lptioo1 41468 qndenserrn 42140 intsaluni 42168 iundjiun 42298 meadjiunlem 42303 meaiininclem 42324 iunhoiioo 42514 |
Copyright terms: Public domain | W3C validator |