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

Theorem opex 4414
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  |-  <. A ,  B >.  e.  _V

Proof of Theorem opex
StepHypRef Expression
1 dfopif 3968 . 2  |-  <. A ,  B >.  =  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )
2 prex 4393 . . 3  |-  { { A } ,  { A ,  B } }  e.  _V
3 0ex 4326 . . 3  |-  (/)  e.  _V
42, 3ifex 3784 . 2  |-  if ( ( A  e.  _V  /\  B  e.  _V ) ,  { { A } ,  { A ,  B } } ,  (/) )  e. 
_V
51, 4eqeltri 2500 1  |-  <. A ,  B >.  e.  _V
Colors of variables: wff set class
Syntax hints:    /\ wa 359    e. wcel 1725   _Vcvv 2943   (/)c0 3615   ifcif 3726   {csn 3801   {cpr 3802   <.cop 3804
This theorem is referenced by:  otex  4415  otth2  4426  oteqex2  4435  oteqex  4436  euop2  4443  opabid  4448  elopab  4449  opabn0  4472  opeliunxp  4915  elvvv  4923  opbrop  4941  relsnop  4966  xpiindi  4996  raliunxp  5000  intirr  5238  xpnz  5278  dmsnn0  5321  dmsnopg  5327  cnvcnvsn  5333  op2ndb  5339  opswap  5342  cnviin  5395  funopg  5471  dffv2  5782  fsn  5892  fvsn  5912  resfunexg  5943  idref  5965  fveqf1o  6015  fliftel  6017  fliftel1  6018  oprabid  6091  dfoprab2  6107  rnoprab  6142  eloprabga  6146  ot1stg  6347  ot2ndg  6348  ot3rdg  6349  fo1st  6352  fo2nd  6353  eloprabi  6399  fpar  6436  algrflem  6441  frxp  6442  xporderlem  6443  fnwelem  6447  mpt2xopoveq  6456  brtpos  6474  dmtpos  6477  rntpos  6478  tpostpos  6485  opiota  6521  tfrlem11  6635  seqomlem1  6693  seqomlem3  6695  seqomlem4  6696  omeu  6814  iiner  6962  th3qlem2  6997  xpsnen  7178  xpcomco  7184  xpassen  7188  xpmapenlem  7260  unxpdomlem1  7299  fseqenlem2  7890  cda1dif  8040  fpwwe  8505  addpipq2  8797  addpqnq  8799  mulpipq2  8800  mulpqnq  8802  ordpipq  8803  prlem934  8894  addsrpr  8934  mulsrpr  8935  addcnsr  8994  mulcnsr  8995  ltresr  8999  addcnsrec  9002  mulcnsrec  9003  axcnre  9023  om2uzrdg  11279  uzrdg0i  11282  uzrdgsuci  11283  hashfun  11683  s1len  11741  s111  11745  wrdexb  11746  fsumcnv  12540  ruclem1  12813  ruclem4  12816  eucalgval2  13055  crt  13150  phimullem  13151  setsval  13476  setsres  13478  setscom  13480  strfv  13484  setsid  13491  imasaddfnlem  13736  imasaddvallem  13737  imasvscafn  13745  idfuval  14056  cofuval  14062  resfval  14072  resfval2  14073  elhoma  14170  xpcco  14263  xpcid  14269  1stfval  14271  2ndfval  14274  prfval  14279  prf1  14280  prf2  14282  evlfval  14297  curfval  14303  curf1  14305  curfcl  14312  hofval  14332  grpss  14809  efgmval  15327  efgi  15334  efgi2  15340  frgpnabllem1  15467  frgpnabllem2  15468  opsrtoslem2  16528  txcnp  17635  upxp  17638  uptx  17640  txdis1cn  17650  hauseqlcld  17661  txlm  17663  xkoinjcn  17702  txflf  18021  divstgplem  18133  ucnima  18294  ucnprima  18295  fmucndlem  18304  imasdsf1olem  18386  cnheiborlem  18962  ovollb2lem  19367  ovolctb  19369  ovolshftlem1  19388  ovolscalem1  19392  ovolicc1  19395  ioombl1lem3  19437  ioombl1lem4  19438  ioorval  19449  dyadval  19467  mbfimaopnlem  19530  limccnp2  19762  nbgraop  21419  2trllemA  21533  constr1trl  21571  1pthonlem1  21572  1pthonlem2  21573  1pthon  21574  2pthon  21585  2pthon3v  21587  constr3lem2  21616  ex-br  21722  grposn  21786  gidsn  21919  ginvsn  21920  rngosn  21975  rngosn3  21997  zrdivrng  22003  cnnvg  22152  cnnvs  22155  cnnvnm  22156  h2hva  22460  h2hsm  22461  h2hnm  22462  hhssva  22742  hhsssm  22743  hhssnm  22744  hhshsslem1  22750  xppreima2  24043  ofpreima  24064  erdszelem9  24868  erdszelem10  24869  txpcon  24902  txsconlem  24910  ghomsn  25082  brtpid1  25161  brtpid2  25162  brtpid3  25163  fprodcnv  25291  brtp  25356  dfpo2  25362  br8  25363  br6  25364  br4  25365  br1steq  25380  br2ndeq  25381  dfdm5  25382  dfrn5  25383  wfrlem14  25519  brv  25667  brtxp  25670  brpprod  25675  brpprod3b  25677  brsset  25679  brtxpsd  25684  dffun10  25704  brcart  25722  brimg  25727  brapply  25728  brcup  25729  brcap  25730  brsuccf  25731  brrestrict  25739  dfrdg4  25740  tfrqfree  25741  brbtwn  25781  brcgr  25782  fvtransport  25909  brcolinear2  25935  colineardim1  25938  brsegle  25985  fvline  26021  ellines  26029  mblfinlem  26185  filnetlem3  26341  heiborlem6  26457  heiborlem7  26458  heiborlem8  26459  otthg  27994  el2wlkonotot0  28111  bnj97  28989  bnj553  29021  bnj966  29067  bnj1442  29170  dvhvaddval  31619  dvhvscaval  31628  dibglbN  31695  dihglbcpreN  31829  dihmeetlem4preN  31835  dihmeetlem13N  31848  hdmapfval  32359
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411  ax-sep 4317  ax-nul 4325  ax-pr 4390
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-ne 2595  df-v 2945  df-dif 3310  df-un 3312  df-in 3314  df-ss 3321  df-nul 3616  df-if 3727  df-sn 3807  df-pr 3808  df-op 3810
  Copyright terms: Public domain W3C validator