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 4778 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2an 691 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 205 ∧ wa 397 ∈ wcel 2107 Vcvv 3444 ⊆ wss 3909 {cpr 4587 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2709 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2716 df-cleq 2730 df-clel 2816 df-v 3446 df-un 3914 df-in 3916 df-ss 3926 df-sn 4586 df-pr 4588 |
This theorem is referenced by: tpss 4794 uniintsn 4947 pwssun 5526 xpsspw 5762 dffv2 6932 fiint 9202 wunex2 10608 hashfun 14265 fun2dmnop0 14321 prdsle 17279 prdsless 17280 prdsleval 17294 pwsle 17309 acsfn2 17478 joinfval 18197 joindmss 18203 meetfval 18211 meetdmss 18217 clatl 18332 ipoval 18354 ipolerval 18356 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 27680 structgrssvtx 27761 structgrssiedg 27762 umgredg 27875 wlk1walk 28373 wlkonl1iedg 28399 wlkdlem2 28417 3wlkdlem6 28895 frcond2 28997 frcond3 28999 nfrgr2v 29002 frgr3vlem1 29003 frgr3vlem2 29004 2pthfrgrrn 29012 frgrncvvdeqlem2 29030 shincli 30090 chincli 30188 lsmsnorb 31953 quslsm 31967 coinfliprv 32843 altxpsspw 34448 mnurndlem1 42294 fourierdlem103 44160 fourierdlem104 44161 nnsum3primes4 45680 |
Copyright terms: Public domain | W3C validator |