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 4748: 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 4748 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2anc 584 | 1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2105 ⊆ wss 3935 {cpr 4561 |
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 2793 |
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 2800 df-cleq 2814 df-clel 2893 df-nfc 2963 df-v 3497 df-un 3940 df-in 3942 df-ss 3951 df-sn 4560 df-pr 4562 |
This theorem is referenced by: fpr2g 6966 f1prex 7031 fveqf1o 7049 fr3nr 7482 en2eqpr 9422 en2eleq 9423 r0weon 9427 wuncval2 10158 nehash2 13822 1idssfct 16014 basprssdmsets 16539 mrcun 16883 joinval2 17609 meetval2 17623 0idnsgd 18263 pmtrprfv 18512 pmtrprfv3 18513 symggen 18529 pmtr3ncomlem1 18532 psgnunilem1 18552 lspprcl 19681 lsptpcl 19682 lspprss 19695 lspprid1 19700 lsppratlem2 19851 lsppratlem3 19852 lsppratlem4 19853 drngnidl 19932 drnglpir 19956 mdetralt 21147 topgele 21468 pptbas 21546 isconn2 21952 xpsdsval 22920 itgioo 24345 wilthlem2 25574 perfectlem2 25734 upgrex 26805 upgr1e 26826 uspgr1e 26954 eupth2lems 27945 s2f1 30549 pmtrcnel 30661 pmtrcnel2 30662 pmtridf1o 30664 cycpm2tr 30689 cyc3co2 30710 cyc3evpm 30720 cyc3genpmlem 30721 cyc3conja 30727 linds2eq 30869 poimirlem9 34783 clsk1indlem4 40274 clsk1indlem1 40275 mnuprssd 40485 mnuprdlem4 40491 limsup10exlem 41933 meadjun 42625 line2 44637 line2y 44640 |
Copyright terms: Public domain | W3C validator |