Theorem opex 2782

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 2416	. 2 |- <.A, B>. = {{A}, {A, B}}
2		prex 2781	. 2 |- {{A}, {A, B}} e. V
3	1, 2	eqeltr 1544	1 |- <.A, B>. e. V

Syntax hints:   e. wcel 958  Vcvv 1811  {csn 2409  {cpr 2410  <.cop 2411

This theorem is referenced by:  otthg 2790  oteqex 2799  euop2 2806  opabid 2810  elopab 2811  ssopab2 2822  opabn0 2824  opbrop 3238  dmsn0 3324  dmsnsn0 3325  dmsnop 3328  cnvsn 3449  op2ndb 3451  xpnz 3466  unixp0 3518  funsn 3543  funopg 3547  fvsn 3794  fsn 3834  tfrlem11 3921  dfoprab2 3991  rnoprab 4004  eloprabg 4007  fo1st 4091  fo2nd 4092  1st2val 4095  2nd2val 4096  2ndconst 4097  brecop 4306  brecop2 4307  ecopoprdm 4309  eceqopreq 4313  th3qlem2 4315  xpsnen 4435  xpcomen 4439  xpassen 4441  xpmapenlem4 4499  xpmapenlem5 4500  enqeceq 5047  addpipq 5054  mulpipq 5055  distrpqlem 5066  enreceq 5177  addsrpr 5184  mulsrpr 5185  addcnsr 5253  mulcnsr 5254  ltresr 5258  supre 5260  addcnsrec 5263  mulcnsrec 5264  axrnegex 5283  axrrecex 5284  axcnre 5286  ltxrt 5495  seq1lem1 6309  seq1rval 6311  seq11lem 6315  seqzfval 6537  ruclem6 7515  ruclem7 7516  ruclem8 7517  ruclem15 7524  xplmi 7973  xplm 7975  xpcn 7976  oprcn 7977  grpsn 8124  ringsn 8163  nvvcop 8213  nvex 8230  nvoprne 8306  cnnvg 8308  cnnvs 8311  cnnvnm 8312  abscn 8343  h2hva 8843  h2hsm 8844  h2hnm 8845  hhssva 9129  hhsssm 9130  hhssnm 9131  hhshsslem1 9137  hhsssh2 9140  ghomsn 10388  elo 10444  stcat 10457  1alg 10654  eloi 10659  1ded 10671  1cat 10692

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-11 967  ax-12 968  ax-13 969  ax-14 970  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459  ax-sep 2703  ax-pow 2742  ax-pr 2779

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 981  df-sb 1172  df-eu 1382  df-mo 1383  df-clab 1464  df-cleq 1469  df-clel 1472  df-ne 1587  df-v 1812  df-dif 2049  df-un 2050  df-in 2051  df-ss 2053  df-nul 2281  df-pw 2402  df-sn 2412  df-pr 2413  df-op 2416

Copyright terms: Public domain