Theorem opex 5474

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	⊢ ⟨𝐴, 𝐵⟩ ∈ V

Proof of Theorem opex

Step	Hyp	Ref	Expression
1		dfopif 4874	. 2 ⊢ ⟨𝐴, 𝐵⟩ = if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅)
2		prex 5442	. . 3 ⊢ {{𝐴}, {𝐴, 𝐵}} ∈ V
3		0ex 5312	. . 3 ⊢ ∅ ∈ V
4	2, 3	ifex 4580	. 2 ⊢ if((𝐴 ∈ V ∧ 𝐵 ∈ V), {{𝐴}, {𝐴, 𝐵}}, ∅) ∈ V
5	1, 4	eqeltri 2834	1 ⊢ ⟨𝐴, 𝐵⟩ ∈ V

Syntax hints:   ∧ wa 395   ∈ wcel 2105  Vcvv 3477  ∅c0 4338  ifcif 4530  {csn 4630  {cpr 4632  ⟨cop 4636

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705  ax-sep 5301  ax-nul 5311  ax-pr 5437

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-dif 3965  df-un 3967  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637

This theorem is referenced by:  otex  5475  brv  5482  otth2  5493  otthg  5495  sbcop1  5498  oteqex2  5508  oteqex  5509  snopeqop  5515  propeqop  5516  propssopi  5517  euop2  5521  brsnop  5531  brtp  5532  opabidw  5533  opabid  5534  elopab  5536  rexopabb  5537  opabn0  5562  opeliunxp  5755  elvvv  5763  opbrop  5785  relsnopg  5815  xpiindi  5848  raliunxp  5852  idrefALT  6133  intirr  6140  xpnz  6180  dmsnn0  6228  dmsnopg  6234  cnvcnvsn  6240  op2ndb  6248  opswap  6250  cnviin  6307  reuop  6314  dfpo2  6317  funopg  6601  dffv2  7003  fsn  7154  f1o2sn  7161  idref  7165  funsndifnop  7170  fmptsng  7187  fmptsnd  7188  fvsng  7199  resfunexg  7234  fveqf1o  7321  fliftel  7328  fliftel1  7329  oprabidw  7461  oprabid  7462  dfoprab2  7490  oprabv  7492  rnoprab  7536  eloprabga  7540  eloprabgaOLD  7541  ot1stg  8026  ot2ndg  8027  ot3rdg  8028  fo1st  8032  fo2nd  8033  br1steqg  8034  br2ndeqg  8035  opiota  8082  eloprabi  8086  mposn  8126  fpar  8139  fsplitfpar  8141  opco1  8146  opco2  8147  frxp  8149  xporderlem  8150  fnwelem  8154  fvproj  8157  fimaproj  8158  xpord2lem  8165  xpord2pred  8168  xpord2indlem  8170  frxp3  8174  mpoxopoveq  8242  brtpos  8258  dmtpos  8261  rntpos  8262  tpostpos  8269  wfrlem14OLD  8360  tfrlem11  8426  seqomlem1  8488  seqomlem3  8490  seqomlem4  8491  omeu  8621  naddcllem  8712  iiner  8827  xpsnen  9093  xpcomco  9100  xpassen  9104  xpmapenlem  9182  dif1en  9198  dif1enOLD  9200  unxpdomlem1  9283  inlresf  9951  inrresf  9953  djur  9956  djuss  9957  djuun  9963  1stinl  9964  2ndinl  9965  1stinr  9966  2ndinr  9967  fseqenlem2  10062  dju1dif  10210  fpwwe  10683  addpipq2  10973  addpqnq  10975  mulpipq2  10976  mulpqnq  10978  ordpipq  10979  prlem934  11070  addcnsr  11172  mulcnsr  11173  ltresr  11177  addcnsrec  11180  mulcnsrec  11181  axcnre  11201  om2uzrdg  13993  uzrdg0i  13996  uzrdgsuci  13997  hashfun  14472  wrdexb  14559  s1len  14640  s1nz  14641  s111  14649  wrdlen2i  14977  brintclab  15036  fsumcnv  15805  fprodcnv  16015  ruclem1  16263  ruclem4  16266  eucalgval2  16614  crth  16811  phimullem  16812  setsval  17200  setsdm  17203  setsfun  17204  setsfun0  17205  setsexstruct2  17208  setsres  17211  setscom  17213  strfv  17237  setsid  17241  imasaddfnlem  17574  imasaddvallem  17575  imasvscafn  17583  idfuval  17926  cofuval  17932  resfval  17942  resfval2  17943  elhoma  18085  embedsetcestrclem  18212  xpcco  18238  xpcid  18244  1stfval  18246  2ndfval  18249  prfval  18254  prf1  18255  prf2  18257  evlfval  18273  curfval  18279  curf1  18281  curfcl  18288  hofval  18308  intopsn  18679  mgm1  18683  sgrp1  18754  mnd1  18804  mnd1id  18805  grpss  18984  grp1  19077  symg2bas  19424  efgmval  19744  efgi  19751  efgi2  19757  frgpnabllem1  19905  frgpnabllem2  19906  ring1  20323  rngqiprngimfv  21325  rngqiprngimf1  21327  opsrtoslem2  22097  mat1dimelbas  22492  mat1dimbas  22493  mat1dimscm  22496  mat1dimmul  22497  mat1f1o  22499  mat1rhmelval  22501  mvmulfval  22563  m2detleib  22652  txcnp  23643  upxp  23646  uptx  23648  txdis1cn  23658  hauseqlcld  23669  txlm  23671  xkoinjcn  23710  txflf  24029  qustgplem  24144  ucnima  24305  ucnprima  24306  fmucndlem  24315  imasdsf1olem  24398  cnheiborlem  24999  ovollb2lem  25536  ovolctb  25538  ovolshftlem1  25557  ovolscalem1  25561  ovolicc1  25564  ioombl1lem3  25608  ioombl1lem4  25609  ioorval  25622  dyadval  25640  mbfimaopnlem  25703  limccnp2  25941  addsval  28009  mulsval  28149  precsexlem1  28245  precsexlem2  28246  precsexlem3  28247  om2noseqrdg  28324  noseqrdg0  28327  noseqrdgsuc  28328  brbtwn  28928  brcgr  28929  eengbas  29010  ebtwntg  29011  ecgrtg  29012  elntg  29013  structvtxval  29052  structgrssvtx  29055  structgrssiedg  29056  gropd  29062  isuhgrop  29101  uhgrunop  29106  upgrop  29125  upgr0eop  29145  upgrunop  29150  umgrunop  29152  isuspgrop  29192  isusgrop  29193  ausgrusgrb  29196  usgr0eop  29277  griedg0ssusgr  29296  uhgrspanop  29327  uhgrspan1  29334  upgrres  29337  umgrres  29338  usgrres  29339  upgrres1  29344  umgrres1  29345  usgrres1  29346  usgrexi  29472  cusgrexi  29474  cffldtocusgr  29478  cffldtocusgrOLD  29479  cusgrres  29480  vtxdgop  29502  umgr2v2e  29557  wlkp1lem2  29706  wlkswwlksf1o  29908  wwlksnext  29922  eupth2eucrct  30245  eupthvdres  30263  konigsbergumgr  30279  numclwwlk1lem2fv  30384  numclwlk1lem1  30397  ex-br  30459  ex-fpar  30490  cnnvg  30706  cnnvs  30708  cnnvnm  30709  h2hva  31002  h2hsm  31003  h2hnm  31004  hhssva  31285  hhsssm  31286  hhssnm  31287  hhshsslem1  31295  br8d  32629  xppreima2  32667  aciunf1lem  32678  ofpreima  32681  cnvoprabOLD  32737  rlocaddval  33254  rlocmulval  33255  linds2eq  33388  smatrcl  33756  smatlem  33757  txomap  33794  qtophaus  33796  hgt750lemb  34649  bnj97  34858  bnj553  34890  bnj966  34936  bnj1442  35041  erdszelem9  35183  erdszelem10  35184  txpconn  35216  txsconnlem  35224  goel  35331  goeleq12bg  35333  gonafv  35334  gonanegoal  35336  sat1el2xp  35363  fmlaomn0  35374  gonan0  35376  goaln0  35377  gonarlem  35378  gonar  35379  goalrlem  35380  goalr  35381  fmla0disjsuc  35382  fmlasucdisj  35383  satffunlem  35385  satffunlem1lem1  35386  satffunlem2lem1  35388  satfv0fvfmla0  35397  sategoelfvb  35403  prv1n  35415  msubval  35509  mvhval  35518  msubvrs  35544  brtpid1  35700  brtpid2  35701  brtpid3  35702  br8  35735  br6  35736  br4  35737  dfdm5  35753  dfrn5  35754  elima4  35756  fv1stcnv  35757  fv2ndcnv  35758  brtxp  35861  brpprod  35866  brpprod3b  35868  brsset  35870  brtxpsd  35875  dffun10  35895  elfuns  35896  brcart  35913  brimg  35918  brapply  35919  brcup  35920  brcap  35921  brsuccf  35922  brrestrict  35930  dfrecs2  35931  dfrdg4  35932  fvtransport  36013  brcolinear2  36039  colineardim1  36042  brsegle  36089  fvline  36125  ellines  36133  filnetlem3  36362  bj-inftyexpitaufo  37184  bj-inftyexpitaudisj  37187  bj-inftyexpiinv  37190  bj-inftyexpidisj  37192  bj-elccinfty  37196  bj-minftyccb  37207  finxpreclem2  37372  finxp0  37373  finxp1o  37374  finxpreclem3  37375  finxpreclem4  37376  finxpreclem5  37377  finxpreclem6  37378  poimirlem9  37615  poimirlem15  37621  poimirlem17  37623  poimirlem20  37626  poimirlem24  37630  poimirlem28  37634  mblfinlem2  37644  heiborlem6  37802  heiborlem7  37803  heiborlem8  37804  grposnOLD  37868  rngosn3  37910  gidsn  37938  zrdivrng  37939  brxrn  38355  br1cossxrnres  38429  dvhvaddval  41072  dvhvscaval  41081  dibglbN  41148  dihglbcpreN  41282  dihmeetlem4preN  41288  dihmeetlem13N  41301  hdmapfval  41809  elcnvlem  43590  cotrintab  43603  elimaint  43638  snhesn  43775  projf1o  45139  dvnprodlem1  45901  dvnprodlem2  45902  sge0xp  46384  hoicvr  46503  hoicvrrex  46511  hoidmv1le  46549  hoi2toco  46562  ovnlecvr2  46565  ovolval5lem2  46608  fsetsnf1  47001  setsidel  47300  prproropf1olem3  47429  prproropf1olem4  47430  prproropreud  47433  isisubgr  47785  ushggricedg  47833  gpgusgralem  47945  gpgvtxedg0  47955  gpgvtxedg1  47956  gpg5nbgrvtx03starlem1  47958  gpg5nbgrvtx03starlem2  47959  gpg5nbgrvtx03starlem3  47960  gpg5nbgrvtx13starlem1  47961  gpg5nbgrvtx13starlem2  47962  gpg5nbgrvtx13starlem3  47963  gpg3nbgrvtx0  47966  gpg3nbgrvtx0ALT  47967  gpg3nbgrvtx1  47968  gpg5nbgrvtx03star  47970  gpg5nbgr3star  47971  opeliun2xp  48177  lmod1lem2  48333  lmod1lem3  48334  lmod1zr  48338  zlmodzxznm  48342  zlmodzxzldeplem  48343  rrx2xpref1o  48567  line2x  48603  inlinecirc02plem  48635  thincciso  48848  mndtchom  48892