Theorem preq1 2444

Description: An equality theorem for unordered pairs.

Assertion

Ref	Expression
preq1	|- (A = B -> {A, C} = {B, C})

Proof of Theorem preq1

Step	Hyp	Ref	Expression
1		sneq 2413	. . 3 |- (A = B -> {A} = {B})
2	1	uneq1d 2179	. 2 |- (A = B -> ({A} u. {C}) = ({B} u. {C}))
3		df-pr 2409	. 2 |- {A, C} = ({A} u. {C})
4		df-pr 2409	. 2 |- {B, C} = ({B} u. {C})
5	2, 3, 4	3eqtr4g 1528	1 |- (A = B -> {A, C} = {B, C})

Syntax hints:   -> wi 3   = wceq 954   u. cun 2041  {csn 2405  {cpr 2406

This theorem is referenced by:  preq2 2445  prssg 2468  preq12b 2479  opeq1 2483  opprc1 2494  uniprg 2511  prex 2776  opthwiener 2802  relop 3270  funopg 3539  opthreg 4584  aceq6b 4722  brdom7disj 4784  brdom6disj 4785  metxpdval 7781  sshjval3t 9264  intprd 10403

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 960  ax-gen 961  ax-8 962  ax-10 964  ax-12 966  ax-17 969  ax-4 971  ax-5o 973  ax-6o 976  ax-9o 1121  ax-10o 1138  ax-16 1208  ax-11o 1216  ax-ext 1457

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-ex 979  df-sb 1170  df-clab 1462  df-cleq 1467  df-clel 1470  df-v 1808  df-un 2046  df-sn 2408  df-pr 2409

Copyright terms: Public domain