Theorem opex 2858

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 2474	. 2 |- <.A, B>. = {{A}, {A, B}}
2		prex 2857	. 2 |- {{A}, {A, B}} e. V
3	1, 2	eqeltri 1587	1 |- <.A, B>. e. V

Syntax hints:   e. wcel 994  Vcvv 1857  {csn 2467  {cpr 2468  <.cop 2469

This theorem is referenced by:  otthg 2866  oteqex 2875  euop2 2883  opabid 2887  elopab 2888  ssopab2 2900  opabn0 2902  elvvv 3314  opbrop 3324  xpnz 3551  dmsnop 3577  cnvsn 3580  opswap 3581  op2ndb 3583  unixp0 3623  funsn 3648  funopg 3652  iunfopab 3719  fvsn 3906  fsn 3948  dfoprab2 4050  rnoprab 4064  eloprabg 4067  fo1st 4152  fo2nd 4153  fparlem1 4199  fparlem2 4200  fparlem3 4201  fparlem4 4202  fpar 4203  tfrlem11 4222  brecop 4447  brecop2 4448  ecopoprdm 4450  eceqopreq 4454  th3qlem2 4456  xpsnen 4576  xpcomen 4580  xpassen 4582  ac6sfilem3 4590  xpmapenlem4 4646  xpmapenlem5 4647  enqeceq 5201  addpipq 5208  mulpipq 5209  distrpqlem 5220  enreceq 5331  addsrpr 5338  mulsrpr 5339  addcnsr 5407  mulcnsr 5408  ltresr 5412  supre 5414  addcnsrec 5417  mulcnsrec 5418  axrnegex 5437  axrrecex 5438  axcnre 5440  ltxr 5649  seq1lem1 6674  seq1rval 6676  seq11lem 6680  seqzfval 6732  ruclem6 7727  ruclem7 7728  ruclem8 7729  ruclem15 7736  xplmi 8184  xplm 8186  xpcn 8187  oprcn 8188  grpsn 8273  ringsn 8405  nvvcop 8460  nvex 8477  nvoprne 8553  cnnvg 8555  cnnvs 8558  cnnvnm 8559  abscn 8597  h2hva 9118  h2hsm 9119  h2hnm 9120  hhssva 9405  hhsssm 9406  hhssnm 9407  hhshsslem1 9413  hhsssh2 9416  ghomsn 10673  elo 10733  stcat 10741  eloi 10817  on1el3 10962  on1el4 10963  zrdivrng 10969  1alg 11176  1ded 11192  1cat 11213  extrdom 11236  extrcod 11237  extrcmp 11238  extrid 11239  hartog 11436  filnetlem1 11763  filnetlem3 11765  filnetlem5 11767  filnet 11768  ssga 11777  gapmlem 11783  gapm 11784  oprabopabf 11807  upxp 11822  uptx 11978  txcnopab 11980

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-11 1003  ax-12 1004  ax-13 1005  ax-14 1006  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500  ax-sep 2777  ax-pow 2818  ax-pr 2855

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-eu 1421  df-mo 1422  df-clab 1506  df-cleq 1511  df-clel 1514  df-ne 1630  df-v 1858  df-dif 2101  df-un 2102  df-in 2103  df-ss 2105  df-nul 2333  df-pw 2459  df-sn 2470  df-pr 2471  df-op 2474

Copyright terms: Public domain