Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > prssd | Structured version Visualization version GIF version |
Description: Deduction version of prssi 4746: A pair of elements of a class is a subset of the class. (Contributed by Glauco Siliprandi, 17-Aug-2020.) |
Ref | Expression |
---|---|
prssd.1 | ⊢ (𝜑 → 𝐴 ∈ 𝐶) |
prssd.2 | ⊢ (𝜑 → 𝐵 ∈ 𝐶) |
Ref | Expression |
---|---|
prssd | ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prssd.1 | . 2 ⊢ (𝜑 → 𝐴 ∈ 𝐶) | |
2 | prssd.2 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝐶) | |
3 | prssi 4746 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ⊆ wss 3933 {cpr 4559 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1787 ax-4 1801 ax-5 1902 ax-6 1961 ax-7 2006 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2151 ax-12 2167 ax-ext 2790 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 842 df-3an 1081 df-tru 1531 df-ex 1772 df-nf 1776 df-sb 2061 df-clab 2797 df-cleq 2811 df-clel 2890 df-nfc 2960 df-v 3494 df-un 3938 df-in 3940 df-ss 3949 df-sn 4558 df-pr 4560 |
This theorem is referenced by: fpr2g 6965 f1prex 7031 fveqf1o 7049 fr3nr 7483 en2eqpr 9421 en2eleq 9422 r0weon 9426 wuncval2 10157 nehash2 13820 1idssfct 16012 basprssdmsets 16537 mrcun 16881 joinval2 17607 meetval2 17621 0idnsgd 18261 pmtrprfv 18510 pmtrprfv3 18511 symggen 18527 pmtr3ncomlem1 18530 psgnunilem1 18550 lspprcl 19679 lsptpcl 19680 lspprss 19693 lspprid1 19698 lsppratlem2 19849 lsppratlem3 19850 lsppratlem4 19851 drngnidl 19930 drnglpir 19954 mdetralt 21145 topgele 21466 pptbas 21544 isconn2 21950 xpsdsval 22918 itgioo 24343 wilthlem2 25573 perfectlem2 25733 upgrex 26804 upgr1e 26825 uspgr1e 26953 eupth2lems 27944 s2f1 30548 pmtrcnel 30660 pmtrcnel2 30661 pmtridf1o 30663 cycpm2tr 30688 cyc3co2 30709 cyc3evpm 30719 cyc3genpmlem 30720 cyc3conja 30726 linds2eq 30868 poimirlem9 34782 clsk1indlem4 40272 clsk1indlem1 40273 mnuprssd 40482 mnuprdlem4 40488 limsup10exlem 41929 meadjun 42621 line2 44667 line2y 44670 |
Copyright terms: Public domain | W3C validator |