![]() |
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 4495 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2an 710 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 383 ∈ wcel 2139 Vcvv 3340 ⊆ wss 3715 {cpr 4323 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1871 ax-4 1886 ax-5 1988 ax-6 2054 ax-7 2090 ax-9 2148 ax-10 2168 ax-11 2183 ax-12 2196 ax-13 2391 ax-ext 2740 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-3an 1074 df-tru 1635 df-ex 1854 df-nf 1859 df-sb 2047 df-clab 2747 df-cleq 2753 df-clel 2756 df-nfc 2891 df-v 3342 df-un 3720 df-in 3722 df-ss 3729 df-sn 4322 df-pr 4324 |
This theorem is referenced by: tpss 4513 uniintsn 4666 pwssun 5170 xpsspw 5389 dffv2 6434 fpr2g 6640 fiint 8404 wunex2 9772 hashfun 13436 fun2dmnop0 13488 prdsle 16344 prdsless 16345 prdsleval 16359 pwsle 16374 acsfn2 16545 joinfval 17222 joindmss 17228 meetfval 17236 meetdmss 17242 clatl 17337 ipoval 17375 ipolerval 17377 eqgfval 17863 eqgval 17864 gaorb 17960 pmtrrn2 18100 efgcpbllema 18387 frgpuplem 18405 drngnidl 19451 drnglpir 19475 isnzr2hash 19486 ltbval 19693 ltbwe 19694 opsrle 19697 opsrtoslem1 19706 thlle 20263 isphtpc 23014 axlowdimlem4 26045 structgrssvtx 26133 structgrssiedg 26134 structgrssvtxlemOLD 26135 structgrssvtxOLD 26136 structgrssiedgOLD 26137 umgredg 26253 wlk1walk 26766 wlkonl1iedg 26792 wlkdlem2 26811 3wlkdlem6 27338 frcond2 27442 frcond3 27444 nfrgr2v 27447 frgr3vlem1 27448 frgr3vlem2 27449 2pthfrgrrn 27457 frgrncvvdeqlem2 27475 shincli 28551 chincli 28649 coinfliprv 30874 altxpsspw 32411 fourierdlem103 40947 fourierdlem104 40948 nnsum3primes4 42204 |
Copyright terms: Public domain | W3C validator |