Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > opeq2 | GIF version |
Description: Equality theorem for ordered pairs. (Contributed by NM, 25-Jun-1998.) (Revised by Mario Carneiro, 26-Apr-2015.) |
Ref | Expression |
---|---|
opeq2 | ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq1 2233 | . . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi2d 461 | . . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V))) |
3 | eqidd 2171 | . . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶} = {𝐶}) | |
4 | preq2 3661 | . . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
5 | 3, 4 | preq12d 3668 | . . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}}) |
6 | 5 | eleq2d 2240 | . . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})) |
7 | 2, 6 | anbi12d 470 | . . . 4 ⊢ (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))) |
8 | df-3an 975 | . . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})) | |
9 | df-3an 975 | . . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})) | |
10 | 7, 8, 9 | 3bitr4g 222 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))) |
11 | 10 | abbidv 2288 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}) |
12 | df-op 3592 | . 2 ⊢ 〈𝐶, 𝐴〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} | |
13 | df-op 3592 | . 2 ⊢ 〈𝐶, 𝐵〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})} | |
14 | 11, 12, 13 | 3eqtr4g 2228 | 1 ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 973 = wceq 1348 ∈ wcel 2141 {cab 2156 Vcvv 2730 {csn 3583 {cpr 3584 〈cop 3586 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 704 ax-5 1440 ax-7 1441 ax-gen 1442 ax-ie1 1486 ax-ie2 1487 ax-8 1497 ax-10 1498 ax-11 1499 ax-i12 1500 ax-bndl 1502 ax-4 1503 ax-17 1519 ax-i9 1523 ax-ial 1527 ax-i5r 1528 ax-ext 2152 |
This theorem depends on definitions: df-bi 116 df-3an 975 df-tru 1351 df-nf 1454 df-sb 1756 df-clab 2157 df-cleq 2163 df-clel 2166 df-nfc 2301 df-v 2732 df-un 3125 df-sn 3589 df-pr 3590 df-op 3592 |
This theorem is referenced by: opeq12 3767 opeq2i 3769 opeq2d 3772 oteq2 3775 oteq3 3776 breq2 3993 cbvopab2 4063 cbvopab2v 4066 opthg 4223 eqvinop 4228 opelopabsb 4245 opelxp 4641 opabid2 4742 elrn2g 4801 opeldm 4814 opeldmg 4816 elrn2 4853 opelresg 4898 iss 4937 elimasng 4979 issref 4993 dmsnopg 5082 cnvsng 5096 elxp4 5098 elxp5 5099 dffun5r 5210 funopg 5232 f1osng 5483 tz6.12f 5525 fsn 5668 fsng 5669 fvsng 5692 oveq2 5861 cbvoprab2 5926 ovg 5991 opabex3d 6100 opabex3 6101 op1stg 6129 op2ndg 6130 oprssdmm 6150 op1steq 6158 dfoprab4f 6172 tfrlemibxssdm 6306 tfr1onlembxssdm 6322 tfrcllembxssdm 6335 elixpsn 6713 ixpsnf1o 6714 mapsnen 6789 xpsnen 6799 xpassen 6808 xpf1o 6822 djulclr 7026 djurclr 7027 djulcl 7028 djurcl 7029 djulclb 7032 inl11 7042 djuss 7047 1stinl 7051 2ndinl 7052 1stinr 7053 2ndinr 7054 elreal 7790 ax1rid 7839 fseq1p1m1 10050 cnmpt21 13085 djucllem 13835 |
Copyright terms: Public domain | W3C validator |