Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > preq1 | Structured version Visualization version GIF version |
Description: Equality theorem for unordered pairs. (Contributed by NM, 29-Mar-1998.) |
Ref | Expression |
---|---|
preq1 | ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sneq 4187 | . . 3 ⊢ (𝐴 = 𝐵 → {𝐴} = {𝐵}) | |
2 | 1 | uneq1d 3766 | . 2 ⊢ (𝐴 = 𝐵 → ({𝐴} ∪ {𝐶}) = ({𝐵} ∪ {𝐶})) |
3 | df-pr 4180 | . 2 ⊢ {𝐴, 𝐶} = ({𝐴} ∪ {𝐶}) | |
4 | df-pr 4180 | . 2 ⊢ {𝐵, 𝐶} = ({𝐵} ∪ {𝐶}) | |
5 | 2, 3, 4 | 3eqtr4g 2681 | 1 ⊢ (𝐴 = 𝐵 → {𝐴, 𝐶} = {𝐵, 𝐶}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1483 ∪ cun 3572 {csn 4177 {cpr 4179 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-v 3202 df-un 3579 df-sn 4178 df-pr 4180 |
This theorem is referenced by: preq2 4269 preq12 4270 preq1i 4271 preq1d 4274 tpeq1 4277 prnzgOLD 4312 preq1b 4377 preq12b 4382 preq12bg 4386 prel12g 4387 elpreqpr 4396 elpr2elpr 4398 opeq1 4402 uniprg 4450 intprg 4511 prex 4909 propeqop 4970 fprg 6422 fnpr2g 6474 opthreg 8515 brdom7disj 9353 brdom6disj 9354 wunpr 9531 wunex2 9560 wuncval2 9569 grupr 9619 wwlktovf 13699 joindef 17004 meetdef 17018 pptbas 20812 usgredg4 26109 usgredg2vlem2 26118 usgredg2v 26119 nbgrval 26234 nb3grprlem2 26283 cusgredg 26320 cusgrfilem2 26352 usgredgsscusgredg 26355 rusgrnumwrdl2 26482 usgr2trlncl 26656 crctcshwlkn0lem6 26707 rusgrnumwwlks 26869 upgr3v3e3cycl 27040 upgr4cycl4dv4e 27045 eupth2lem3lem4 27091 nfrgr2v 27136 frgr3vlem1 27137 frgr3vlem2 27138 3vfriswmgr 27142 3cyclfrgrrn1 27149 4cycl2vnunb 27154 vdgn1frgrv2 27160 frgrncvvdeqlem8 27170 frgrncvvdeqlem9 27171 frgrwopregasn 27180 frgrwopreglem5ALT 27186 extwwlkfablem1 27207 altopthsn 32068 hdmap11lem2 37134 sge0prle 40618 meadjun 40679 elsprel 41725 prelspr 41736 sprsymrelfolem2 41743 |
Copyright terms: Public domain | W3C validator |