![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > prssi | GIF version |
Description: A pair of elements of a class is a subset of the class. (Contributed by NM, 16-Jan-2015.) |
Ref | Expression |
---|---|
prssi | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | prssg 3709 | . 2 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) ↔ {𝐴, 𝐵} ⊆ 𝐶)) | |
2 | 1 | ibi 175 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐶) → {𝐴, 𝐵} ⊆ 𝐶) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∈ wcel 2125 ⊆ wss 3098 {cpr 3557 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1424 ax-7 1425 ax-gen 1426 ax-ie1 1470 ax-ie2 1471 ax-8 1481 ax-10 1482 ax-11 1483 ax-i12 1484 ax-bndl 1486 ax-4 1487 ax-17 1503 ax-i9 1507 ax-ial 1511 ax-i5r 1512 ax-ext 2136 |
This theorem depends on definitions: df-bi 116 df-tru 1335 df-nf 1438 df-sb 1740 df-clab 2141 df-cleq 2147 df-clel 2150 df-nfc 2285 df-v 2711 df-un 3102 df-in 3104 df-ss 3111 df-sn 3562 df-pr 3563 |
This theorem is referenced by: tpssi 3718 prelpwi 4169 onun2 4443 onintexmid 4526 nnregexmid 4574 en2eqpr 6841 m1expcl2 10419 m1expcl 10420 minmax 11106 xrminmax 11139 1idssfct 11963 unopn 12342 bdop 13388 012of 13506 isomninnlem 13542 trilpolemisumle 13550 trilpolemeq1 13552 trilpolemlt1 13553 iswomninnlem 13561 iswomni0 13563 ismkvnnlem 13564 nconstwlpolemgt0 13575 |
Copyright terms: Public domain | W3C validator |