|   | 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 4818 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
| 4 | 1, 2, 3 | mp2an 692 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) | 
| Colors of variables: wff setvar class | 
| Syntax hints: ↔ wb 206 ∧ wa 395 ∈ wcel 2107 Vcvv 3479 ⊆ wss 3950 {cpr 4627 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-v 3481 df-un 3955 df-ss 3967 df-sn 4626 df-pr 4628 | 
| This theorem is referenced by: tpss 4836 uniintsn 4984 pwssun 5574 xpsspw 5818 dffv2 7003 fiint 9367 fiintOLD 9368 wunex2 10779 hashfun 14477 fun2dmnop0 14544 prdsle 17508 prdsless 17509 prdsleval 17523 pwsle 17538 acsfn2 17707 joinfval 18419 joindmss 18425 meetfval 18433 meetdmss 18439 clatl 18554 ipoval 18576 ipolerval 18578 eqgfval 19195 eqgval 19196 eqg0subg 19215 gaorb 19326 pmtrrn2 19479 efgcpbllema 19773 frgpuplem 19791 isnzr2hash 20520 thlle 21717 thlleOLD 21718 ltbval 22062 ltbwe 22063 opsrle 22066 opsrtoslem1 22080 isphtpc 25027 axlowdimlem4 28961 structgrssvtx 29042 structgrssiedg 29043 umgredg 29156 wlk1walk 29658 wlkonl1iedg 29684 wlkdlem2 29702 3wlkdlem6 30185 frcond2 30287 frcond3 30289 nfrgr2v 30292 frgr3vlem1 30293 frgr3vlem2 30294 2pthfrgrrn 30302 frgrncvvdeqlem2 30320 shincli 31382 chincli 31480 lsmsnorb 33420 quslsm 33434 coinfliprv 34486 altxpsspw 35979 mnurndlem1 44305 fourierdlem103 46229 fourierdlem104 46230 nnsum3primes4 47780 isubgr3stgrlem6 47943 grlimgrtrilem2 47967 | 
| Copyright terms: Public domain | W3C validator |