Theorem opex 4654

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 4155	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4632	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4525	. . 3 |- (/) e. _V
4	2, 3	ifex 3952	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2486	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 367   e. wcel 1842   _Vcvv 3058   (/)c0 3737   ifcif 3884   {csn 3971   {cpr 3973   <.cop 3977

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-sep 4516  ax-nul 4524  ax-pr 4629

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-v 3060  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-sn 3972  df-pr 3974  df-op 3978

This theorem is referenced by:  otex  4655  otth2  4671  otthg  4673  oteqex2  4681  oteqex  4682  euop2  4689  opabid  4696  elopab  4697  opabn0  4720  opeliunxp  4874  elvvv  4882  opbrop  4902  relsnop  4927  xpiindi  4958  raliunxp  4962  intirr  5205  xpnz  5243  dmsnn0  5288  dmsnopg  5294  cnvcnvsn  5300  op2ndb  5307  opswap  5310  cnviin  5360  funopg  5600  dffv2  5921  fsn  6047  f1o2sn  6053  fmptsng  6071  fmptsnd  6072  fvsn  6083  fpr2g  6111  resfunexg  6117  idref  6133  fveqf1o  6187  fliftel  6189  fliftel1  6190  oprabid  6304  dfoprab2  6323  oprabv  6325  rnoprab  6365  eloprabga  6369  ot1stg  6797  ot2ndg  6798  ot3rdg  6799  fo1st  6803  fo2nd  6804  opiota  6842  eloprabi  6845  mpt2sn  6874  fpar  6887  algrflem  6892  frxp  6893  xporderlem  6894  fnwelem  6898  mpt2xopoveq  6949  brtpos  6966  dmtpos  6969  rntpos  6970  tpostpos  6977  wfrlem14  7033  tfrlem11  7090  seqomlem1  7151  seqomlem3  7153  seqomlem4  7154  omeu  7270  iiner  7419  xpsnen  7638  xpcomco  7644  xpassen  7648  xpmapenlem  7721  unxpdomlem1  7758  fseqenlem2  8437  cda1dif  8587  fpwwe  9053  addpipq2  9343  addpqnq  9345  mulpipq2  9346  mulpqnq  9348  ordpipq  9349  prlem934  9440  addcnsr  9541  mulcnsr  9542  ltresr  9546  addcnsrec  9549  mulcnsrec  9550  axcnre  9570  om2uzrdg  12106  uzrdg0i  12109  uzrdgsuci  12110  hashfun  12542  wrdexb  12608  s1len  12669  s111  12675  wrdlen2i  12938  brintclab  12982  fsumcnv  13737  fprodcnv  13937  ruclem1  14171  ruclem4  14174  eucalgval2  14417  crt  14515  phimullem  14516  setsval  14864  setsres  14869  setscom  14871  strfv  14875  setsid  14882  imasaddfnlem  15140  imasaddvallem  15141  imasvscafn  15149  idfuval  15487  cofuval  15493  resfval  15503  resfval2  15504  elhoma  15633  embedsetcestrclem  15748  xpcco  15774  xpcid  15780  1stfval  15782  2ndfval  15785  prfval  15790  prf1  15791  prf2  15793  evlfval  15808  curfval  15814  curf1  15816  curfcl  15823  hofval  15843  intopsn  16204  mgm1  16206  sgrp1  16240  mnd1  16283  mnd1OLD  16284  mnd1id  16285  grpss  16393  grp1  16464  symg2bas  16745  efgmval  17052  efgi  17059  efgi2  17065  frgpnabllem1  17199  frgpnabllem2  17200  ring1  17566  opsrtoslem2  18467  mat1dimelbas  19263  mat1dimbas  19264  mat1dimscm  19267  mat1dimmul  19268  mat1f1o  19270  mat1rhmelval  19272  mvmulfval  19334  m2detleib  19423  txcnp  20411  upxp  20414  uptx  20416  txdis1cn  20426  hauseqlcld  20437  txlm  20439  xkoinjcn  20478  txflf  20797  qustgplem  20909  ucnima  21074  ucnprima  21075  fmucndlem  21084  imasdsf1olem  21166  cnheiborlem  21744  ovollb2lem  22189  ovolctb  22191  ovolshftlem1  22210  ovolscalem1  22214  ovolicc1  22217  ioombl1lem3  22260  ioombl1lem4  22261  ioorval  22273  dyadval  22291  mbfimaopnlem  22352  limccnp2  22586  brbtwn  24606  brcgr  24607  eengbas  24688  ebtwntg  24689  ecgrtg  24690  elntg  24691  edgopval  24744  nbgraop  24827  nbgraopALT  24828  2trllemA  24956  constr1trl  24994  1pthonlem1  24995  1pthonlem2  24996  1pthon  24997  2pthon  25008  2pthon3v  25010  constr3lem2  25050  wlkiswwlksur  25123  wwlknext  25128  el2wlkonotot0  25276  numclwlk1lem2fv  25497  ex-br  25556  grposn  25617  gidsn  25750  ginvsn  25751  rngosn  25806  rngosn3  25828  zrdivrng  25834  cnnvg  25983  cnnvs  25986  cnnvnm  25987  h2hva  26291  h2hsm  26292  h2hnm  26293  hhssva  26575  hhsssm  26576  hhssnm  26577  hhshsslem1  26583  br8d  27886  xppreima2  27917  aciunf1lem  27932  ofpreima  27936  cnvoprab  27979  fvproj  28274  fimaproj  28275  txomap  28276  qtophaus  28278  bnj97  29238  bnj553  29270  bnj966  29316  bnj1442  29419  erdszelem9  29483  erdszelem10  29484  txpcon  29516  txsconlem  29524  msubval  29724  mvhval  29733  msubvrs  29759  ghomsn  29867  brtpid1  29914  brtpid2  29915  brtpid3  29916  brtp  29949  dfpo2  29955  br8  29956  br6  29957  br4  29958  br1steq  29974  br2ndeq  29975  dfdm5  29978  dfrn5  29979  elima4  29981  fv1stcnv  29982  fv2ndcnv  29983  brv  30202  brtxp  30205  brpprod  30210  brpprod3b  30212  brsset  30214  brtxpsd  30219  dffun10  30239  elfuns  30240  brcart  30257  brimg  30262  brapply  30263  brcup  30264  brcap  30265  brsuccf  30266  brrestrict  30274  dfrecs2  30275  dfrdg4  30276  fvtransport  30357  brcolinear2  30383  colineardim1  30386  brsegle  30433  fvline  30469  ellines  30477  filnetlem3  30595  bj-inftyexpiinv  31162  bj-inftyexpidisj  31164  bj-elccinfty  31168  bj-minftyccb  31179  mblfinlem2  31404  heiborlem6  31574  heiborlem7  31575  heiborlem8  31576  dvhvaddval  34090  dvhvscaval  34099  dibglbN  34166  dihglbcpreN  34300  dihmeetlem4preN  34306  dihmeetlem13N  34319  hdmapfval  34830  elimaint  35607  snhesn  35747  dvnprodlem1  37092  dvnprodlem2  37093  gordopval  38000  gsizopval  38001  usgfis  38056  opeliun2xp  38414  lmod1lem2  38581  lmod1lem3  38582  lmod1zr  38586  zlmodzxznm  38590  zlmodzxzldeplem  38591