opex - Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
Unicode version

Theorem opex 2772

Description: An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16.

**Assertion**
Ref	Expression
opex

**Proof of Theorem opex**
Step	Hyp	Ref	Expression
1		df-op 2406	. 2
2		prex 2771	. 2
3	1, 2	eqeltr 1536	1

Colors of variables: wff set class

Syntax hints:

wcel 955

cvv 1802

csn 2399

cpr 2400

cop 2401

This theorem is referenced by: otthg 2780 euop2 2795 opabid 2799 elopab 2800 ssopab2 2811 opabn0 2813 opbrop 3228 dmsn0 3313 dmsnsn0 3314 dmsnop 3317 cnvsn 3435 op2ndb 3437 xpnz 3452 unixp0 3504 funsn 3529 funopg 3533 fvsn 3779 fsn 3819 tfrlem11 3906 dfoprab2 3976 rnoprab 3989 eloprabg 3992 fo1st 4075 fo2nd 4076 1st2val 4079 2nd2val 4080 2ndconst 4081 brecop 4290 brecop2 4291 ecopoprdm 4293 eceqopreq 4297 th3qlem2 4299 xpsnen 4415 xpcomen 4419 xpassen 4421 xpmapenlem4 4479 xpmapenlem5 4480 enqeceq 5019 addpipq 5026 mulpipq 5027 distrpqlem 5038 enreceq 5149 addsrpr 5156 mulsrpr 5157 addcnsr 5225 mulcnsr 5226 ltresr 5230 supre 5232 addcnsrec 5235 mulcnsrec 5236 axrnegex 5255 axrrecex 5256 axcnre 5258 ltxrt 5467 seq1lem1 6246 seq1rval 6248 seq11lem 6252 seqzfval 6469 ruclem6 7458 ruclem7 7459 ruclem8 7460 ruclem15 7467 xplmi 7907 xplm 7909 xpcn 7910 oprcn 7911 grpsn 8061 ablsn 8062 ringsn 8100 nvvcop 8151 nvex 8169 cnnvg 8246 cnnvs 8249 cnnvnm 8250 abscn 8277 h2hva 8782 h2hsm 8783 h2hnm 8784 hhssva 9050 hhsssm 9051 hhssnm 9052 hhshsslem1 9057 ghomsn 10293 elo 10345 stcat 10353 1alg 10498 eloi 10503 1ded 10515 1cat 10536

This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 ax-7 959 ax-gen 960 ax-8 961 ax-10 963 ax-11 964 ax-12 965 ax-13 966 ax-14 967 ax-17 968 ax-4 970 ax-5o 972 ax-6o 975 ax-9o 1119 ax-10o 1136 ax-16 1206 ax-11o 1213 ax-ext 1452 ax-sep 2693 ax-pow 2732 ax-pr 2769

This theorem depends on definitions: df-bi 147 df-or 224 df-an 225 df-ex 978 df-sb 1168 df-eu 1375 df-mo 1376 df-clab 1457 df-cleq 1462 df-clel 1465 df-ne 1579 df-v 1803 df-dif 2039 df-un 2040 df-in 2041 df-ss 2043 df-nul 2271 df-pw 2392 df-sn 2402 df-pr 2403 df-op 2406