Theorem opex 4387

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 3941	. 2 |- <. A , B >. = if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) )
2		prex 4366	. . 3 |- { { A } , { A , B } } e. _V
3		0ex 4299	. . 3 |- (/) e. _V
4	2, 3	ifex 3757	. 2 |- if ( ( A e. _V /\ B e. _V ) , { { A } , { A , B } } , (/) ) e. _V
5	1, 4	eqeltri 2474	1 |- <. A , B >. e. _V

Syntax hints:   /\ wa 359   e. wcel 1721   _Vcvv 2916   (/)c0 3588   ifcif 3699   {csn 3774   {cpr 3775   <.cop 3777

This theorem is referenced by:  otex  4388  otth2  4399  oteqex2  4408  oteqex  4409  euop2  4416  opabid  4421  elopab  4422  opabn0  4445  opeliunxp  4888  elvvv  4896  opbrop  4914  relsnop  4939  xpiindi  4969  raliunxp  4973  intirr  5211  xpnz  5251  dmsnn0  5294  dmsnopg  5300  cnvcnvsn  5306  op2ndb  5312  opswap  5315  cnviin  5368  funopg  5444  dffv2  5755  fsn  5865  fvsn  5885  resfunexg  5916  idref  5938  fveqf1o  5988  fliftel  5990  fliftel1  5991  oprabid  6064  dfoprab2  6080  rnoprab  6115  eloprabga  6119  ot1stg  6320  ot2ndg  6321  ot3rdg  6322  fo1st  6325  fo2nd  6326  eloprabi  6372  fpar  6409  algrflem  6414  frxp  6415  xporderlem  6416  fnwelem  6420  mpt2xopoveq  6429  brtpos  6447  dmtpos  6450  rntpos  6451  tpostpos  6458  opiota  6494  tfrlem11  6608  seqomlem1  6666  seqomlem3  6668  seqomlem4  6669  omeu  6787  iiner  6935  th3qlem2  6970  xpsnen  7151  xpcomco  7157  xpassen  7161  xpmapenlem  7233  unxpdomlem1  7272  fseqenlem2  7862  cda1dif  8012  fpwwe  8477  addpipq2  8769  addpqnq  8771  mulpipq2  8772  mulpqnq  8774  ordpipq  8775  prlem934  8866  addsrpr  8906  mulsrpr  8907  addcnsr  8966  mulcnsr  8967  ltresr  8971  addcnsrec  8974  mulcnsrec  8975  axcnre  8995  om2uzrdg  11251  uzrdg0i  11254  uzrdgsuci  11255  hashfun  11655  s1len  11713  s111  11717  wrdexb  11718  fsumcnv  12512  ruclem1  12785  ruclem4  12788  eucalgval2  13027  crt  13122  phimullem  13123  setsval  13448  setsres  13450  setscom  13452  strfv  13456  setsid  13463  imasaddfnlem  13708  imasaddvallem  13709  imasvscafn  13717  idfuval  14028  cofuval  14034  resfval  14044  resfval2  14045  elhoma  14142  xpcco  14235  xpcid  14241  1stfval  14243  2ndfval  14246  prfval  14251  prf1  14252  prf2  14254  evlfval  14269  curfval  14275  curf1  14277  curfcl  14284  hofval  14304  grpss  14781  efgmval  15299  efgi  15306  efgi2  15312  frgpnabllem1  15439  frgpnabllem2  15440  opsrtoslem2  16500  txcnp  17605  upxp  17608  uptx  17610  txdis1cn  17620  hauseqlcld  17631  txlm  17633  xkoinjcn  17672  txflf  17991  divstgplem  18103  ucnima  18264  ucnprima  18265  fmucndlem  18274  imasdsf1olem  18356  cnheiborlem  18932  ovollb2lem  19337  ovolctb  19339  ovolshftlem1  19358  ovolscalem1  19362  ovolicc1  19365  ioombl1lem3  19407  ioombl1lem4  19408  ioorval  19419  dyadval  19437  mbfimaopnlem  19500  limccnp2  19732  nbgraop  21389  2trllemA  21503  constr1trl  21541  1pthonlem1  21542  1pthonlem2  21543  1pthon  21544  2pthon  21555  2pthon3v  21557  constr3lem2  21586  ex-br  21692  grposn  21756  gidsn  21889  ginvsn  21890  rngosn  21945  rngosn3  21967  zrdivrng  21973  cnnvg  22122  cnnvs  22125  cnnvnm  22126  h2hva  22430  h2hsm  22431  h2hnm  22432  hhssva  22712  hhsssm  22713  hhssnm  22714  hhshsslem1  22720  xppreima2  24013  ofpreima  24034  erdszelem9  24838  erdszelem10  24839  txpcon  24872  txsconlem  24880  ghomsn  25052  brtpid1  25131  brtpid2  25132  brtpid3  25133  fprodcnv  25260  brtp  25320  dfpo2  25326  br8  25327  br6  25328  br4  25329  br1steq  25344  br2ndeq  25345  dfdm5  25346  dfrn5  25347  wfrlem14  25483  brv  25631  brtxp  25634  brpprod  25639  brpprod3b  25641  brsset  25643  brtxpsd  25648  brcart  25685  brimg  25690  brapply  25691  brcup  25692  brcap  25693  brsuccf  25694  brrestrict  25702  dfrdg4  25703  tfrqfree  25704  brbtwn  25742  brcgr  25743  fvtransport  25870  brcolinear2  25896  colineardim1  25899  brsegle  25946  fvline  25982  ellines  25990  mblfinlem  26143  filnetlem3  26299  heiborlem6  26415  heiborlem7  26416  heiborlem8  26417  otthg  27952  el2wlkonotot0  28069  bnj97  28943  bnj553  28975  bnj966  29021  bnj1442  29124  dvhvaddval  31573  dvhvscaval  31582  dibglbN  31649  dihglbcpreN  31783  dihmeetlem4preN  31789  dihmeetlem13N  31802  hdmapfval  32313

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385  ax-sep 4290  ax-nul 4298  ax-pr 4363

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ne 2569  df-v 2918  df-dif 3283  df-un 3285  df-in 3287  df-ss 3294  df-nul 3589  df-if 3700  df-sn 3780  df-pr 3781  df-op 3783