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 4755 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
4 | 1, 2, 3 | mp2an 690 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 ∈ wcel 2113 Vcvv 3497 ⊆ wss 3939 {cpr 4572 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1969 ax-7 2014 ax-8 2115 ax-9 2123 ax-10 2144 ax-11 2160 ax-12 2176 ax-ext 2796 |
This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1539 df-ex 1780 df-nf 1784 df-sb 2069 df-clab 2803 df-cleq 2817 df-clel 2896 df-nfc 2966 df-v 3499 df-un 3944 df-in 3946 df-ss 3955 df-sn 4571 df-pr 4573 |
This theorem is referenced by: tpss 4771 uniintsn 4916 pwssun 5459 xpsspw 5685 dffv2 6759 fiint 8798 wunex2 10163 hashfun 13801 fun2dmnop0 13855 prdsle 16738 prdsless 16739 prdsleval 16753 pwsle 16768 acsfn2 16937 joinfval 17614 joindmss 17620 meetfval 17628 meetdmss 17634 clatl 17729 ipoval 17767 ipolerval 17769 eqgfval 18331 eqgval 18332 gaorb 18440 pmtrrn2 18591 efgcpbllema 18883 frgpuplem 18901 isnzr2hash 20040 ltbval 20255 ltbwe 20256 opsrle 20259 opsrtoslem1 20267 thlle 20844 isphtpc 23601 axlowdimlem4 26734 structgrssvtx 26812 structgrssiedg 26813 umgredg 26926 wlk1walk 27423 wlkonl1iedg 27450 wlkdlem2 27468 3wlkdlem6 27947 frcond2 28049 frcond3 28051 nfrgr2v 28054 frgr3vlem1 28055 frgr3vlem2 28056 2pthfrgrrn 28064 frgrncvvdeqlem2 28082 shincli 29142 chincli 29240 lsmsnorb 30949 coinfliprv 31744 altxpsspw 33442 mnurndlem1 40623 fourierdlem103 42501 fourierdlem104 42502 nnsum3primes4 43960 |
Copyright terms: Public domain | W3C validator |