Theorem opex 4577

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 4077	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4555	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4443	. . 3 |- (/) e. _V
4	2, 3	ifex 3879	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2513	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 369   e. wcel 1756   _Vcvv 2993   (/)c0 3658   ifcif 3812   {csn 3898   {cpr 3900   <.cop 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pr 4552

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-v 2995  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905

This theorem is referenced by:  otex  4578  otth2  4594  oteqex2  4604  oteqex  4605  euop2  4612  opabid  4617  elopab  4618  opabn0  4640  opeliunxp  4911  elvvv  4919  opbrop  4937  relsnop  4965  xpiindi  4996  raliunxp  5000  intirr  5237  xpnz  5278  dmsnn0  5325  dmsnopg  5331  cnvcnvsn  5337  op2ndb  5344  opswap  5347  cnviin  5395  funopg  5471  dffv2  5785  fsn  5902  fmptsng  5921  fvsn  5932  resfunexg  5964  idref  5979  fveqf1o  6021  fliftel  6023  fliftel1  6024  oprabid  6136  dfoprab2  6154  rnoprab  6194  eloprabga  6198  ot1stg  6612  ot2ndg  6613  ot3rdg  6614  fo1st  6617  fo2nd  6618  opiota  6654  eloprabi  6657  fpar  6697  algrflem  6702  frxp  6703  xporderlem  6704  fnwelem  6708  mpt2xopoveq  6757  brtpos  6775  dmtpos  6778  rntpos  6779  tpostpos  6786  tfrlem11  6868  seqomlem1  6926  seqomlem3  6928  seqomlem4  6929  omeu  7045  iiner  7193  th3qlem2  7228  xpsnen  7416  xpcomco  7422  xpassen  7426  xpmapenlem  7499  unxpdomlem1  7538  fseqenlem2  8216  cda1dif  8366  fpwwe  8834  addpipq2  9126  addpqnq  9128  mulpipq2  9129  mulpqnq  9131  ordpipq  9132  prlem934  9223  addsrpr  9263  mulsrpr  9264  addcnsr  9323  mulcnsr  9324  ltresr  9328  addcnsrec  9331  mulcnsrec  9332  axcnre  9352  om2uzrdg  11800  uzrdg0i  11803  uzrdgsuci  11804  hashfun  12220  wrdexb  12266  s1len  12317  s111  12323  wrdlen2i  12567  fsumcnv  13261  ruclem1  13534  ruclem4  13537  eucalgval2  13777  crt  13874  phimullem  13875  setsval  14219  setsres  14223  setscom  14225  strfv  14229  setsid  14236  imasaddfnlem  14487  imasaddvallem  14488  imasvscafn  14496  idfuval  14807  cofuval  14813  resfval  14823  resfval2  14824  elhoma  14921  xpcco  15014  xpcid  15020  1stfval  15022  2ndfval  15025  prfval  15030  prf1  15031  prf2  15033  evlfval  15048  curfval  15054  curf1  15056  curfcl  15063  hofval  15083  grpss  15580  symg2bas  15924  efgmval  16230  efgi  16237  efgi2  16243  frgpnabllem1  16372  frgpnabllem2  16373  opsrtoslem2  17588  mvmulfval  18375  m2detleib  18459  txcnp  19215  upxp  19218  uptx  19220  txdis1cn  19230  hauseqlcld  19241  txlm  19243  xkoinjcn  19282  txflf  19601  divstgplem  19713  ucnima  19878  ucnprima  19879  fmucndlem  19888  imasdsf1olem  19970  cnheiborlem  20548  ovollb2lem  20993  ovolctb  20995  ovolshftlem1  21014  ovolscalem1  21018  ovolicc1  21021  ioombl1lem3  21063  ioombl1lem4  21064  ioorval  21076  dyadval  21094  mbfimaopnlem  21155  limccnp2  21389  brbtwn  23167  brcgr  23168  eengbas  23249  ebtwntg  23250  ecgrtg  23251  elntg  23252  nbgraop  23357  2trllemA  23471  constr1trl  23509  1pthonlem1  23510  1pthonlem2  23511  1pthon  23512  2pthon  23523  2pthon3v  23525  constr3lem2  23554  ex-br  23660  grposn  23724  gidsn  23857  ginvsn  23858  rngosn  23913  rngosn3  23935  zrdivrng  23941  cnnvg  24090  cnnvs  24093  cnnvnm  24094  h2hva  24398  h2hsm  24399  h2hnm  24400  hhssva  24682  hhsssm  24683  hhssnm  24684  hhshsslem1  24690  br8d  25964  xppreima2  25987  ofpreima  26006  cnvoprab  26045  erdszelem9  27109  erdszelem10  27110  txpcon  27143  txsconlem  27151  ghomsn  27329  brtpid1  27399  brtpid2  27400  brtpid3  27401  fprodcnv  27516  brtp  27581  dfpo2  27587  br8  27588  br6  27589  br4  27590  br1steq  27607  br2ndeq  27608  dfdm5  27609  dfrn5  27610  elima4  27612  wfrlem14  27759  brv  27930  brtxp  27933  brpprod  27938  brpprod3b  27940  brsset  27942  brtxpsd  27947  dffun10  27967  elfuns  27968  brcart  27985  brimg  27990  brapply  27991  brcup  27992  brcap  27993  brsuccf  27994  brrestrict  28002  dfrdg4  28003  tfrqfree  28004  fvtransport  28085  brcolinear2  28111  colineardim1  28114  brsegle  28161  fvline  28197  ellines  28205  mblfinlem2  28455  filnetlem3  28627  heiborlem6  28741  heiborlem7  28742  heiborlem8  28743  otthg  30156  oprabv  30183  wlkiswwlksur  30377  wwlknext  30382  el2wlkonotot0  30417  numclwlk1lem2fv  30712  opeliun2xp  30746  fmptsnd  30748  mpt2sn  30750  f1o2sn  30752  mat1dimelbas  30906  mat1dimbas  30907  mat1dimscm  30910  mat1dimmul  30911  mnd1  31018  grp1  31019  rng1  31022  lmod1lem2  31027  lmod1lem3  31028  lmod1zr  31032  zlmodzxznm  31036  zlmodzxzldeplem  31037  bnj97  31955  bnj553  31987  bnj966  32033  bnj1442  32136  bj-inftyexpiinv  32627  bj-inftyexpidisj  32629  bj-elccinfty  32633  bj-minftyccb  32644  dvhvaddval  34831  dvhvscaval  34840  dibglbN  34907  dihglbcpreN  35041  dihmeetlem4preN  35047  dihmeetlem13N  35060  hdmapfval  35571