Theorem opex 4701

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

Step	Hyp	Ref	Expression
1		dfopif 4199	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4679	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4567	. . 3 |- (/) e. _V
4	2, 3	ifex 3995	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2527	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 369   e. wcel 1804   _Vcvv 3095   (/)c0 3770   ifcif 3926   {csn 4014   {cpr 4016   <.cop 4020

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pr 4676

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-v 3097  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-sn 4015  df-pr 4017  df-op 4021

This theorem is referenced by:  otex  4702  otth2  4718  otthg  4720  oteqex2  4729  oteqex  4730  euop2  4737  opabid  4744  elopab  4745  opabn0  4768  opeliunxp  5041  elvvv  5049  opbrop  5069  relsnop  5097  xpiindi  5128  raliunxp  5132  intirr  5375  xpnz  5416  dmsnn0  5463  dmsnopg  5469  cnvcnvsn  5475  op2ndb  5482  opswap  5485  cnviin  5534  funopg  5610  dffv2  5931  fsn  6054  f1o2sn  6059  fmptsng  6077  fmptsnd  6078  fvsn  6089  resfunexg  6122  idref  6138  fveqf1o  6190  fliftel  6192  fliftel1  6193  oprabid  6308  dfoprab2  6328  oprabv  6330  rnoprab  6370  eloprabga  6374  ot1stg  6799  ot2ndg  6800  ot3rdg  6801  fo1st  6805  fo2nd  6806  opiota  6844  eloprabi  6847  mpt2sn  6876  fpar  6889  algrflem  6894  frxp  6895  xporderlem  6896  fnwelem  6900  mpt2xopoveq  6949  brtpos  6966  dmtpos  6969  rntpos  6970  tpostpos  6977  tfrlem11  7059  seqomlem1  7117  seqomlem3  7119  seqomlem4  7120  omeu  7236  iiner  7385  xpsnen  7603  xpcomco  7609  xpassen  7613  xpmapenlem  7686  unxpdomlem1  7726  fseqenlem2  8409  cda1dif  8559  fpwwe  9027  addpipq2  9317  addpqnq  9319  mulpipq2  9320  mulpqnq  9322  ordpipq  9323  prlem934  9414  addcnsr  9515  mulcnsr  9516  ltresr  9520  addcnsrec  9523  mulcnsrec  9524  axcnre  9544  om2uzrdg  12048  uzrdg0i  12051  uzrdgsuci  12052  hashfun  12476  wrdexb  12539  s1len  12598  s111  12604  wrdlen2i  12865  fsumcnv  13569  fprodcnv  13768  ruclem1  13945  ruclem4  13948  eucalgval2  14191  crt  14289  phimullem  14290  setsval  14637  setsres  14641  setscom  14643  strfv  14647  setsid  14654  imasaddfnlem  14906  imasaddvallem  14907  imasvscafn  14915  idfuval  15223  cofuval  15229  resfval  15239  resfval2  15240  elhoma  15337  xpcco  15430  xpcid  15436  1stfval  15438  2ndfval  15441  prfval  15446  prf1  15447  prf2  15449  evlfval  15464  curfval  15470  curf1  15472  curfcl  15479  hofval  15499  intopsn  15860  mgm1  15862  sgrp1  15896  mnd1  15939  mnd1OLD  15940  mnd1id  15941  grpss  16049  grp1  16120  symg2bas  16401  efgmval  16708  efgi  16715  efgi2  16721  frgpnabllem1  16855  frgpnabllem2  16856  ring1  17226  opsrtoslem2  18127  mat1dimelbas  18950  mat1dimbas  18951  mat1dimscm  18954  mat1dimmul  18955  mat1f1o  18957  mat1rhmelval  18959  mvmulfval  19021  m2detleib  19110  txcnp  20098  upxp  20101  uptx  20103  txdis1cn  20113  hauseqlcld  20124  txlm  20126  xkoinjcn  20165  txflf  20484  qustgplem  20596  ucnima  20761  ucnprima  20762  fmucndlem  20771  imasdsf1olem  20853  cnheiborlem  21431  ovollb2lem  21876  ovolctb  21878  ovolshftlem1  21897  ovolscalem1  21901  ovolicc1  21904  ioombl1lem3  21947  ioombl1lem4  21948  ioorval  21960  dyadval  21978  mbfimaopnlem  22039  limccnp2  22273  brbtwn  24178  brcgr  24179  eengbas  24260  ebtwntg  24261  ecgrtg  24262  elntg  24263  edgopval  24316  nbgraop  24399  nbgraopALT  24400  2trllemA  24528  constr1trl  24566  1pthonlem1  24567  1pthonlem2  24568  1pthon  24569  2pthon  24580  2pthon3v  24582  constr3lem2  24622  wlkiswwlksur  24695  wwlknext  24700  el2wlkonotot0  24848  numclwlk1lem2fv  25069  ex-br  25128  grposn  25193  gidsn  25326  ginvsn  25327  rngosn  25382  rngosn3  25404  zrdivrng  25410  cnnvg  25559  cnnvs  25562  cnnvnm  25563  h2hva  25867  h2hsm  25868  h2hnm  25869  hhssva  26151  hhsssm  26152  hhssnm  26153  hhshsslem1  26159  br8d  27439  xppreima2  27464  ofpreima  27483  cnvoprab  27522  fvproj  27812  fimaproj  27813  txomap  27814  qtophaus  27816  erdszelem9  28620  erdszelem10  28621  txpcon  28654  txsconlem  28662  msubval  28862  mvhval  28871  msubvrs  28897  ghomsn  29005  brtpid1  29075  brtpid2  29076  brtpid3  29077  brtp  29153  dfpo2  29159  br8  29160  br6  29161  br4  29162  br1steq  29179  br2ndeq  29180  dfdm5  29181  dfrn5  29182  elima4  29184  wfrlem14  29331  brv  29502  brtxp  29505  brpprod  29510  brpprod3b  29512  brsset  29514  brtxpsd  29519  dffun10  29539  elfuns  29540  brcart  29557  brimg  29562  brapply  29563  brcup  29564  brcap  29565  brsuccf  29566  brrestrict  29574  dfrdg4  29575  tfrqfree  29576  fvtransport  29657  brcolinear2  29683  colineardim1  29686  brsegle  29733  fvline  29769  ellines  29777  mblfinlem2  30027  filnetlem3  30173  heiborlem6  30287  heiborlem7  30288  heiborlem8  30289  gordopval  32228  gsizopval  32229  usgfis  32284  opeliun2xp  32655  lmod1lem2  32824  lmod1lem3  32825  lmod1zr  32829  zlmodzxznm  32833  zlmodzxzldeplem  32834  bnj97  33657  bnj553  33689  bnj966  33735  bnj1442  33838  bj-inftyexpiinv  34351  bj-inftyexpidisj  34353  bj-elccinfty  34357  bj-minftyccb  34368  dvhvaddval  36557  dvhvscaval  36566  dibglbN  36633  dihglbcpreN  36767  dihmeetlem4preN  36773  dihmeetlem13N  36786  hdmapfval  37297  snhesn  37496