Theorem preq2 4739

Description: Equality theorem for unordered pairs. (Contributed by NM, 15-Jul-1993.)

Assertion

Ref	Expression
preq2	⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Proof of Theorem preq2

Step	Hyp	Ref	Expression
1		preq1 4738	. 2 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶})
2		prcom 4737	. 2 ⊢ {𝐶, 𝐴} = {𝐴, 𝐶}
3		prcom 4737	. 2 ⊢ {𝐶, 𝐵} = {𝐵, 𝐶}
4	1, 2, 3	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵})

Syntax hints:   → wi 4   = wceq 1534  {cpr 4631

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3473  df-un 3952  df-sn 4630  df-pr 4632

This theorem is referenced by:  preq12  4740  preq2i  4742  preq2d  4745  tpeq2  4748  ifpprsnss  4769  preq12bg  4855  prel12g  4865  elpreqprlem  4867  elpr2elpr  4870  opeq2  4875  uniprgOLD  4927  intprgOLD  4987  prex  5434  opth  5478  opeqsng  5505  propeqop  5509  relop  5853  funopg  6587  f1oprswap  6883  fprg  7164  fnprb  7220  fnpr2g  7222  pr2ne  10027  pr2neOLD  10028  prdom2  10029  dfac2b  10153  brdom7disj  10554  brdom6disj  10555  wunpr  10732  wunex2  10761  wuncval2  10770  grupr  10820  prunioo  13490  hashprg  14386  wwlktovf  14939  wwlktovfo  14941  wrd2f1tovbij  14943  joindef  18367  meetdef  18381  lspfixed  21015  hmphindis  23700  upgrex  28904  edglnl  28955  usgredg4  29029  usgredgreu  29030  uspgredg2vtxeu  29032  uspgredg2v  29036  nbgrel  29152  nbupgrel  29157  nbumgrvtx  29158  nbusgreledg  29165  nbgrnself  29171  nb3grprlem1  29192  nb3grprlem2  29193  uvtxel1  29208  uvtxusgrel  29215  cusgredg  29236  usgredgsscusgredg  29272  1egrvtxdg0  29324  ifpsnprss  29436  upgriswlk  29454  uspgrn2crct  29618  wwlksnextfun  29708  wwlksnextsurj  29710  wwlksnextbij  29712  clwlkclwwlklem2  29809  clwwlkinwwlk  29849  clwwlknonex2  29918  upgr1wlkdlem1  29954  upgr3v3e3cycl  29989  upgr4cycl4dv4e  29994  eupth2lem3lem4  30040  frcond1  30075  frgr1v  30080  nfrgr2v  30081  frgr3v  30084  1vwmgr  30085  3vfriswmgrlem  30086  3vfriswmgr  30087  1to2vfriswmgr  30088  3cyclfrgrrn1  30094  4cycl2vnunb  30099  n4cyclfrgr  30100  vdgn1frgrv2  30105  frgrncvvdeqlem3  30110  frgrncvvdeqlem8  30115  frgrwopregbsn  30126  frgrwopreglem5ALT  30131  fusgr2wsp2nb  30143  esumpr2  33686  cplgredgex  34730  altopthsn  35557  dihprrn  40899  dvh3dim  40919  mapdindp2  41194  elsprel  46815  prelspr  46826  sprsymrelfolem2  46833  reupr  46862  reuopreuprim  46866  upgrwlkupwlk  47202  inlinecirc02plem  47859

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »