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 4777 | . 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 3443 ⊆ wss 3908 {cpr 4586 |
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 2708 |
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 2715 df-cleq 2729 df-clel 2815 df-v 3445 df-un 3913 df-in 3915 df-ss 3925 df-sn 4585 df-pr 4587 |
This theorem is referenced by: tpss 4793 uniintsn 4946 pwssun 5525 xpsspw 5761 dffv2 6931 fiint 9201 wunex2 10607 hashfun 14264 fun2dmnop0 14320 prdsle 17278 prdsless 17279 prdsleval 17293 pwsle 17308 acsfn2 17477 joinfval 18196 joindmss 18202 meetfval 18210 meetdmss 18216 clatl 18331 ipoval 18353 ipolerval 18355 eqgfval 18910 eqgval 18911 gaorb 19019 pmtrrn2 19174 efgcpbllema 19465 frgpuplem 19483 isnzr2hash 20657 thlle 21025 thlleOLD 21026 ltbval 21366 ltbwe 21367 opsrle 21370 opsrtoslem1 21384 isphtpc 24279 axlowdimlem4 27692 structgrssvtx 27773 structgrssiedg 27774 umgredg 27887 wlk1walk 28385 wlkonl1iedg 28411 wlkdlem2 28429 3wlkdlem6 28907 frcond2 29009 frcond3 29011 nfrgr2v 29014 frgr3vlem1 29015 frgr3vlem2 29016 2pthfrgrrn 29024 frgrncvvdeqlem2 29042 shincli 30102 chincli 30200 lsmsnorb 31965 quslsm 31979 coinfliprv 32855 altxpsspw 34457 mnurndlem1 42325 fourierdlem103 44203 fourierdlem104 44204 nnsum3primes4 45729 |
Copyright terms: Public domain | W3C validator |