Theorem opex 1893

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

Assertion

Ref	Expression
opex	|- <.A, B>. e. V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		df-op 1815	. 2 |- <.A, B>. = {{A}, {A, B}}
2		prex 1892	. 2 |- {{A}, {A, B}} e. V
3	1, 2	eqeltr 1159	1 |- <.A, B>. e. V

Syntax hints:   e. wcel 1092  Vcvv 1348  {csn 1808  {cpr 1809  <.cop 1810

This theorem is referenced by:  otthg 1900  euop2 1912  opabid 2099  elopab 2110  ssopab2 2119  opbrop 2472  cbvop 2473  dmsn0 2543  dmsnsn0 2544  dmsnop 2547  cnvsn 2636  op2ndb 2638  funsn 2690  fvsn 2879  fsn 2895  tfrlem11 2959  dfoprab2 3021  rnoprab 3033  eloprabg 3035  fo1st 3094  fo2nd 3095  1st2val 3097  brecop 3242  brecop2 3243  ecopoprdm 3245  eceqopreq 3249  th3qlem2 3251  xpsnen 3339  xpcomen 3343  xpassen 3344  xpmapenlem4 3394  xpmapenlem5 3395  enqeceq 3841  addpipq 3848  mulpipq 3849  distrpqlem 3860  enreceq 3971  addsrpr 3978  mulsrpr 3979  addcnsr 4047  mulcnsr 4048  ltresr 4052  supre 4054  addcnsrec 4057  mulcnsrec 4058  axnegex 4078  axrecex 4079  axrnegex 4080  axrrecex 4081  axcnre 4087  seqlem1 4662  seqrval 4664  seq1lem 4668  ruclem6 4890  ruclem7 4891  ruclem13 4897  ruclem15 4899

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-pow 1077

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-v 1349  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-nul 1708  df-pw 1799  df-sn 1811  df-pr 1812  df-op 1815

metamath.org