![]() |
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 4815 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 396 ∈ wcel 2106 Vcvv 3473 ⊆ wss 3944 {cpr 4624 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2702 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2709 df-cleq 2723 df-clel 2809 df-v 3475 df-un 3949 df-in 3951 df-ss 3961 df-sn 4623 df-pr 4625 |
This theorem is referenced by: tpss 4831 uniintsn 4984 pwssun 5564 xpsspw 5801 dffv2 6972 fiint 9307 wunex2 10715 hashfun 14379 fun2dmnop0 14437 prdsle 17390 prdsless 17391 prdsleval 17405 pwsle 17420 acsfn2 17589 joinfval 18308 joindmss 18314 meetfval 18322 meetdmss 18328 clatl 18443 ipoval 18465 ipolerval 18467 eqgfval 19028 eqgval 19029 gaorb 19137 pmtrrn2 19292 efgcpbllema 19586 frgpuplem 19604 isnzr2hash 20248 thlle 21184 thlleOLD 21185 ltbval 21526 ltbwe 21527 opsrle 21530 opsrtoslem1 21544 isphtpc 24439 axlowdimlem4 28068 structgrssvtx 28149 structgrssiedg 28150 umgredg 28263 wlk1walk 28761 wlkonl1iedg 28787 wlkdlem2 28805 3wlkdlem6 29283 frcond2 29385 frcond3 29387 nfrgr2v 29390 frgr3vlem1 29391 frgr3vlem2 29392 2pthfrgrrn 29400 frgrncvvdeqlem2 29418 shincli 30478 chincli 30576 lsmsnorb 32359 quslsm 32374 coinfliprv 33310 altxpsspw 34777 mnurndlem1 42809 fourierdlem103 44696 fourierdlem104 44697 nnsum3primes4 46226 |
Copyright terms: Public domain | W3C validator |