Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > prss | Structured version Visualization version GIF version |
Description: A pair of elements of a class is a subset of the class. Theorem 7.5 of [Quine] p. 49. (Contributed by NM, 30-May-1994.) (Proof shortened by Andrew Salmon, 29-Jun-2011.) (Proof shortened by JJ, 23-Jul-2021.) |
Ref | Expression |
---|---|
prss.1 | ⊢ 𝐴 ∈ V |
prss.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
prss | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prss.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | prss.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | prssg 4290 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2an 704 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 195 ∧ wa 383 ∈ wcel 1977 Vcvv 3173 ⊆ wss 3540 {cpr 4127 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-v 3175 df-un 3545 df-in 3547 df-ss 3554 df-sn 4126 df-pr 4128 |
This theorem is referenced by: tpss 4308 uniintsn 4449 pwssun 4944 xpsspw 5156 dffv2 6181 fpr2g 6380 fiint 8122 wunex2 9439 hashfun 13084 fun2dmnop0 13131 prdsle 15945 prdsless 15946 prdsleval 15960 pwsle 15975 acsfn2 16147 joinfval 16824 joindmss 16830 meetfval 16838 meetdmss 16844 clatl 16939 ipoval 16977 ipolerval 16979 eqgfval 17465 eqgval 17466 gaorb 17563 pmtrrn2 17703 efgcpbllema 17990 frgpuplem 18008 drngnidl 19050 drnglpir 19074 isnzr2hash 19085 ltbval 19292 ltbwe 19293 opsrle 19296 opsrtoslem1 19305 thlle 19860 isphtpc 22601 axlowdimlem4 25625 structgrssvtxlem 25700 structgrssvtx 25701 structgrssiedg 25702 umgredg 25812 usgrarnedg 25913 cusgrarn 25988 frgraun 26523 frisusgranb 26524 frgra2v 26526 frgra3vlem1 26527 frgra3vlem2 26528 2pthfrgrarn 26536 frgrancvvdeqlem3 26559 shincli 27605 chincli 27703 coinfliprv 29871 altxpsspw 31254 fourierdlem103 39102 fourierdlem104 39103 nnsum3primes4 40204 1wlk1walk 40843 wlkOnl1iedg 40873 1wlkdlem2 40892 31wlkdlem6 41332 frcond2 41439 frcond3 41440 nfrgr2v 41442 frgr3vlem1 41443 frgr3vlem2 41444 2pthfrgrrn 41452 frgrncvvdeqlem3 41471 |
Copyright terms: Public domain | W3C validator |