![]() |
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 4820: 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 4820 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) | |
4 | 1, 2, 3 | syl2anc 583 | 1 ⊢ (𝜑 → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∈ wcel 2099 ⊆ wss 3944 {cpr 4626 |
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-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-or 847 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-v 3471 df-un 3949 df-in 3951 df-ss 3961 df-sn 4625 df-pr 4627 |
This theorem is referenced by: fpr2g 7217 f1prex 7287 fveqf1o 7306 fr3nr 7768 en2eqpr 10024 en2eleq 10025 r0weon 10029 wuncval2 10764 nehash2 14461 1idssfct 16644 basprssdmsets 17186 mrcun 17595 joinval2 18366 meetval2 18380 0idnsgd 19119 pmtrprfv 19401 pmtrprfv3 19402 symggen 19418 pmtr3ncomlem1 19421 psgnunilem1 19441 lspprcl 20855 lsptpcl 20856 lspprss 20869 lspprid1 20874 lsppratlem2 21029 lsppratlem3 21030 lsppratlem4 21031 drngnidl 21131 drnglpir 21215 mdetralt 22503 topgele 22825 pptbas 22904 isconn2 23311 xpsdsval 24280 itgioo 25738 wilthlem2 26994 perfectlem2 27156 upgrex 28898 upgr1e 28919 uspgr1e 29050 eupth2lems 30041 s2f1 32662 pmtrcnel 32806 pmtrcnel2 32807 pmtridf1o 32809 cycpm2tr 32834 cyc3co2 32855 cyc3evpm 32865 cyc3genpmlem 32866 cyc3conja 32872 linds2eq 33090 poimirlem9 37091 clsk1indlem4 43446 clsk1indlem1 43447 mnuprssd 43678 mnuprdlem4 43684 limsup10exlem 45132 meadjun 45822 line2 47797 line2y 47800 lubprlem 47953 joindm3 47960 meetdm3 47962 toplatjoin 47985 toplatmeet 47986 |
Copyright terms: Public domain | W3C validator |