MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  opex Unicode version

Theorem opex 4716
Description: An ordered pair of classes is a set. Exercise 7 of [TakeutiZaring] p. 16. (Contributed by NM, 18-Aug-1993.) (Revised by Mario Carneiro, 26-Apr-2015.)
Assertion
Ref Expression
opex

Proof of Theorem opex
StepHypRef Expression
1 dfopif 4214 . 2
2 prex 4694 . . 3
3 0ex 4582 . . 3
42, 3ifex 4010 . 2
51, 4eqeltri 2541 1
Colors of variables: wff setvar class
Syntax hints:  /\wa 369  e.wcel 1818   cvv 3109   c0 3784  ifcif 3941  {csn 4029  {cpr 4031  <.cop 4035
This theorem is referenced by:  otex  4717  otth2  4733  otthg  4735  oteqex2  4744  oteqex  4745  euop2  4752  opabid  4759  elopab  4760  opabn0  4783  opeliunxp  5056  elvvv  5064  opbrop  5084  relsnop  5112  xpiindi  5143  raliunxp  5147  intirr  5390  xpnz  5431  dmsnn0  5478  dmsnopg  5484  cnvcnvsn  5490  op2ndb  5497  opswap  5500  cnviin  5549  funopg  5625  dffv2  5946  fsn  6069  f1o2sn  6074  fmptsng  6092  fmptsnd  6093  fvsn  6104  resfunexg  6137  idref  6153  fveqf1o  6205  fliftel  6207  fliftel1  6208  oprabid  6323  dfoprab2  6343  oprabv  6345  rnoprab  6385  eloprabga  6389  ot1stg  6814  ot2ndg  6815  ot3rdg  6816  fo1st  6820  fo2nd  6821  opiota  6859  eloprabi  6862  mpt2sn  6891  fpar  6904  algrflem  6909  frxp  6910  xporderlem  6911  fnwelem  6915  mpt2xopoveq  6966  brtpos  6983  dmtpos  6986  rntpos  6987  tpostpos  6994  tfrlem11  7076  seqomlem1  7134  seqomlem3  7136  seqomlem4  7137  omeu  7253  iiner  7402  xpsnen  7621  xpcomco  7627  xpassen  7631  xpmapenlem  7704  unxpdomlem1  7744  fseqenlem2  8427  cda1dif  8577  fpwwe  9045  addpipq2  9335  addpqnq  9337  mulpipq2  9338  mulpqnq  9340  ordpipq  9341  prlem934  9432  addcnsr  9533  mulcnsr  9534  ltresr  9538  addcnsrec  9541  mulcnsrec  9542  axcnre  9562  om2uzrdg  12067  uzrdg0i  12070  uzrdgsuci  12071  hashfun  12495  wrdexb  12558  s1len  12617  s111  12623  wrdlen2i  12884  fsumcnv  13588  fprodcnv  13787  ruclem1  13964  ruclem4  13967  eucalgval2  14210  crt  14308  phimullem  14309  setsval  14656  setsres  14660  setscom  14662  strfv  14666  setsid  14673  imasaddfnlem  14925  imasaddvallem  14926  imasvscafn  14934  idfuval  15245  cofuval  15251  resfval  15261  resfval2  15262  elhoma  15359  xpcco  15452  xpcid  15458  1stfval  15460  2ndfval  15463  prfval  15468  prf1  15469  prf2  15471  evlfval  15486  curfval  15492  curf1  15494  curfcl  15501  hofval  15521  intopsn  15882  mgm1  15884  sgrp1  15918  mnd1  15961  mnd1OLD  15962  mnd1id  15963  grpss  16071  grp1  16142  symg2bas  16423  efgmval  16730  efgi  16737  efgi2  16743  frgpnabllem1  16877  frgpnabllem2  16878  ring1  17248  opsrtoslem2  18149  mat1dimelbas  18973  mat1dimbas  18974  mat1dimscm  18977  mat1dimmul  18978  mat1f1o  18980  mat1rhmelval  18982  mvmulfval  19044  m2detleib  19133  txcnp  20121  upxp  20124  uptx  20126  txdis1cn  20136  hauseqlcld  20147  txlm  20149  xkoinjcn  20188  txflf  20507  qustgplem  20619  ucnima  20784  ucnprima  20785  fmucndlem  20794  imasdsf1olem  20876  cnheiborlem  21454  ovollb2lem  21899  ovolctb  21901  ovolshftlem1  21920  ovolscalem1  21924  ovolicc1  21927  ioombl1lem3  21970  ioombl1lem4  21971  ioorval  21983  dyadval  22001  mbfimaopnlem  22062  limccnp2  22296  brbtwn  24202  brcgr  24203  eengbas  24284  ebtwntg  24285  ecgrtg  24286  elntg  24287  edgopval  24340  nbgraop  24423  nbgraopALT  24424  2trllemA  24552  constr1trl  24590  1pthonlem1  24591  1pthonlem2  24592  1pthon  24593  2pthon  24604  2pthon3v  24606  constr3lem2  24646  wlkiswwlksur  24719  wwlknext  24724  el2wlkonotot0  24872  numclwlk1lem2fv  25093  ex-br  25152  grposn  25217  gidsn  25350  ginvsn  25351  rngosn  25406  rngosn3  25428  zrdivrng  25434  cnnvg  25583  cnnvs  25586  cnnvnm  25587  h2hva  25891  h2hsm  25892  h2hnm  25893  hhssva  26175  hhsssm  26176  hhssnm  26177  hhshsslem1  26183  br8d  27463  xppreima2  27488  ofpreima  27507  cnvoprab  27546  fvproj  27835  fimaproj  27836  txomap  27837  qtophaus  27839  erdszelem9  28643  erdszelem10  28644  txpcon  28677  txsconlem  28685  msubval  28885  mvhval  28894  msubvrs  28920  ghomsn  29028  brtpid1  29098  brtpid2  29099  brtpid3  29100  brtp  29178  dfpo2  29184  br8  29185  br6  29186  br4  29187  br1steq  29204  br2ndeq  29205  dfdm5  29206  dfrn5  29207  elima4  29209  wfrlem14  29356  brv  29527  brtxp  29530  brpprod  29535  brpprod3b  29537  brsset  29539  brtxpsd  29544  dffun10  29564  elfuns  29565  brcart  29582  brimg  29587  brapply  29588  brcup  29589  brcap  29590  brsuccf  29591  brrestrict  29599  dfrdg4  29600  tfrqfree  29601  fvtransport  29682  brcolinear2  29708  colineardim1  29711  brsegle  29758  fvline  29794  ellines  29802  mblfinlem2  30052  filnetlem3  30198  heiborlem6  30312  heiborlem7  30313  heiborlem8  30314  dvnprodlem1  31743  dvnprodlem2  31744  gordopval  32390  gsizopval  32391  usgfis  32446  embedsetcestrclem  32663  opeliun2xp  32922  lmod1lem2  33089  lmod1lem3  33090  lmod1zr  33094  zlmodzxznm  33098  zlmodzxzldeplem  33099  bnj97  33924  bnj553  33956  bnj966  34002  bnj1442  34105  bj-inftyexpiinv  34611  bj-inftyexpidisj  34613  bj-elccinfty  34617  bj-minftyccb  34628  dvhvaddval  36817  dvhvscaval  36826  dibglbN  36893  dihglbcpreN  37027  dihmeetlem4preN  37033  dihmeetlem13N  37046  hdmapfval  37557  brintclab  37763  elimaint  37764  snhesn  37809
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036
  Copyright terms: Public domain W3C validator