![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opex | GIF version |
Description: An ordered pair of sets is a set. (Contributed by Jim Kingdon, 24-Sep-2018.) (Revised by Mario Carneiro, 24-May-2019.) |
Ref | Expression |
---|---|
opex.1 | ⊢ 𝐴 ∈ V |
opex.2 | ⊢ 𝐵 ∈ V |
Ref | Expression |
---|---|
opex | ⊢ 〈𝐴, 𝐵〉 ∈ V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | opex.1 | . 2 ⊢ 𝐴 ∈ V | |
2 | opex.2 | . 2 ⊢ 𝐵 ∈ V | |
3 | opexg 4246 | . 2 ⊢ ((𝐴 ∈ V ∧ 𝐵 ∈ V) → 〈𝐴, 𝐵〉 ∈ V) | |
4 | 1, 2, 3 | mp2an 426 | 1 ⊢ 〈𝐴, 𝐵〉 ∈ V |
Colors of variables: wff set class |
Syntax hints: ∈ wcel 2160 Vcvv 2752 〈cop 3610 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-14 2163 ax-ext 2171 ax-sep 4136 ax-pow 4192 ax-pr 4227 |
This theorem depends on definitions: df-bi 117 df-3an 982 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-clel 2185 df-nfc 2321 df-v 2754 df-un 3148 df-in 3150 df-ss 3157 df-pw 3592 df-sn 3613 df-pr 3614 df-op 3616 |
This theorem is referenced by: otth2 4259 opabid 4275 elopab 4276 opabm 4298 elvvv 4707 relsnop 4750 xpiindim 4782 raliunxp 4786 rexiunxp 4787 intirr 5033 xpmlem 5067 dmsnm 5112 dmsnopg 5118 cnvcnvsn 5123 op2ndb 5130 cnviinm 5188 funopg 5269 fsn 5708 fvsn 5731 idref 5777 oprabid 5927 dfoprab2 5942 rnoprab 5978 fo1st 6181 fo2nd 6182 eloprabi 6220 xporderlem 6255 cnvoprab 6258 dmtpos 6280 rntpos 6281 tpostpos 6288 iinerm 6632 th3qlem2 6663 elixpsn 6760 ensn1 6821 mapsnen 6836 xpsnen 6846 xpcomco 6851 xpassen 6855 xpmapenlem 6876 phplem2 6880 ac6sfi 6925 djuss 7098 genipdm 7544 ioof 10000 fsumcnv 11476 fprodcnv 11664 prdsex 12771 txdis1cn 14230 |
Copyright terms: Public domain | W3C validator |