Definition df-pr 4180

Description: Define unordered pair of classes. Definition 7.1 of [Quine] p. 48. For example, A e. { 1 , -u 1 } -> ( A ^ 2 ) = 1 (ex-pr 27287). They are unordered, so { A , B } = { B , A } as proven by prcom 4267. For a more traditional definition, but requiring a dummy variable, see dfpr2 4195. { A , A } is also an unordered pair, but also a singleton because of { A } = { A , A } (see dfsn2 4190). Therefore, { A , B } is called a proper (unordered) pair iff A =/= B and A and B are sets. (Contributed by NM, 21-Jun-1993.)

Assertion

Ref	Expression
df-pr	|- { A , B } = ( { A } u. { B } )

Detailed syntax breakdown of Definition df-pr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	cpr 4179	. 2 class { A , B }
4	1	csn 4177	. . 3 class { A }
5	2	csn 4177	. . 3 class { B }
6	4, 5	cun 3572	. 2 class ( { A } u. { B } )
7	3, 6	wceq 1483	1 wff { A , B } = ( { A } u. { B } )

This definition is referenced by:  dfsn2  4190  dfpr2  4195  ralprg  4234  rexprg  4235  csbprg  4244  disjpr2  4248  disjpr2OLD  4249  prcom  4267  preq1  4268  qdass  4288  qdassr  4289  tpidm12  4290  prprc1  4300  difprsn1  4330  diftpsn3OLD  4333  difpr  4334  tpprceq3  4335  snsspr1  4345  snsspr2  4346  prssg  4350  prssOLD  4352  ssunpr  4365  sstp  4367  iunxprg  4607  iunopeqop  4981  pwssun  5020  xpsspw  5233  dmpropg  5608  rnpropg  5615  funprg  5940  funprgOLD  5941  funtp  5945  fntpg  5948  funcnvpr  5950  f1oprswap  6180  f1oprg  6181  fnimapr  6262  residpr  6409  fpr  6421  fmptpr  6438  fvpr1  6456  fvpr1g  6458  fvpr2g  6459  df2o3  7573  map2xp  8130  1sdom  8163  en2  8196  prfi  8235  prwf  8674  rankprb  8714  pr2nelem  8827  xp2cda  9002  ssxr  10107  prunioo  12301  prinfzo0  12506  fzosplitpr  12577  hashprg  13182  hashprgOLD  13183  hashprlei  13250  s2prop  13652  s4prop  13655  f1oun2prg  13662  sumpr  14477  strlemor2OLD  15970  strle2  15974  phlstr  16034  xpscg  16218  symg2bas  17818  dmdprdpr  18448  dprdpr  18449  lsmpr  19089  lsppr  19093  lspsntri  19097  lsppratlem1  19147  lsppratlem3  19149  lsppratlem4  19150  m2detleib  20437  xpstopnlem1  21612  ovolioo  23336  uniiccdif  23346  i1f1  23457  wilthlem2  24795  perfectlem2  24955  axlowdimlem13  25834  ex-dif  27280  ex-un  27281  ex-in  27282  ex-xp  27293  ex-cnv  27294  ex-rn  27297  ex-res  27298  spanpr  28439  superpos  29213  prct  29492  prodpr  29572  esumpr  30128  eulerpartgbij  30434  signswch  30638  prodfzo03  30681  subfacp1lem1  31161  altopthsn  32068  onint1  32448  poimirlem8  33417  poimirlem9  33418  poimirlem15  33424  smprngopr  33851  dihprrnlem1N  36713  dihprrnlem2  36714  djhlsmat  36716  lclkrlem2c  36798  lclkrlem2v  36817  lcfrlem18  36849  dfrcl4  37968  iunrelexp0  37994  corclrcl  37999  corcltrcl  38031  cotrclrcl  38034  sumpair  39194  rnfdmpr  41300  perfectALTVlem2  41631  xpprsng  42110  gsumpr  42139