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 2227 | . . . . . 6 ⊢ (𝐴 = 𝐵 → (𝐴 ∈ V ↔ 𝐵 ∈ V)) | |
2 | 1 | anbi2d 460 | . . . . 5 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V))) |
3 | eqidd 2165 | . . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶} = {𝐶}) | |
4 | preq2 3648 | . . . . . . 7 ⊢ (𝐴 = 𝐵 → {𝐶, 𝐴} = {𝐶, 𝐵}) | |
5 | 3, 4 | preq12d 3655 | . . . . . 6 ⊢ (𝐴 = 𝐵 → {{𝐶}, {𝐶, 𝐴}} = {{𝐶}, {𝐶, 𝐵}}) |
6 | 5 | eleq2d 2234 | . . . . 5 ⊢ (𝐴 = 𝐵 → (𝑥 ∈ {{𝐶}, {𝐶, 𝐴}} ↔ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})) |
7 | 2, 6 | anbi12d 465 | . . . 4 ⊢ (𝐴 = 𝐵 → (((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))) |
8 | df-3an 969 | . . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ ((𝐶 ∈ V ∧ 𝐴 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})) | |
9 | df-3an 969 | . . . 4 ⊢ ((𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}) ↔ ((𝐶 ∈ V ∧ 𝐵 ∈ V) ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})) | |
10 | 7, 8, 9 | 3bitr4g 222 | . . 3 ⊢ (𝐴 = 𝐵 → ((𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}}) ↔ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}}))) |
11 | 10 | abbidv 2282 | . 2 ⊢ (𝐴 = 𝐵 → {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})}) |
12 | df-op 3579 | . 2 ⊢ 〈𝐶, 𝐴〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐴 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐴}})} | |
13 | df-op 3579 | . 2 ⊢ 〈𝐶, 𝐵〉 = {𝑥 ∣ (𝐶 ∈ V ∧ 𝐵 ∈ V ∧ 𝑥 ∈ {{𝐶}, {𝐶, 𝐵}})} | |
14 | 11, 12, 13 | 3eqtr4g 2222 | 1 ⊢ (𝐴 = 𝐵 → 〈𝐶, 𝐴〉 = 〈𝐶, 𝐵〉) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ∧ w3a 967 = wceq 1342 ∈ wcel 2135 {cab 2150 Vcvv 2721 {csn 3570 {cpr 3571 〈cop 3573 |
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 699 ax-5 1434 ax-7 1435 ax-gen 1436 ax-ie1 1480 ax-ie2 1481 ax-8 1491 ax-10 1492 ax-11 1493 ax-i12 1494 ax-bndl 1496 ax-4 1497 ax-17 1513 ax-i9 1517 ax-ial 1521 ax-i5r 1522 ax-ext 2146 |
This theorem depends on definitions: df-bi 116 df-3an 969 df-tru 1345 df-nf 1448 df-sb 1750 df-clab 2151 df-cleq 2157 df-clel 2160 df-nfc 2295 df-v 2723 df-un 3115 df-sn 3576 df-pr 3577 df-op 3579 |
This theorem is referenced by: opeq12 3754 opeq2i 3756 opeq2d 3759 oteq2 3762 oteq3 3763 breq2 3980 cbvopab2 4050 cbvopab2v 4053 opthg 4210 eqvinop 4215 opelopabsb 4232 opelxp 4628 opabid2 4729 elrn2g 4788 opeldm 4801 opeldmg 4803 elrn2 4840 opelresg 4885 iss 4924 elimasng 4966 issref 4980 dmsnopg 5069 cnvsng 5083 elxp4 5085 elxp5 5086 dffun5r 5194 funopg 5216 f1osng 5467 tz6.12f 5509 fsn 5651 fsng 5652 fvsng 5675 oveq2 5844 cbvoprab2 5906 ovg 5971 opabex3d 6081 opabex3 6082 op1stg 6110 op2ndg 6111 oprssdmm 6131 op1steq 6139 dfoprab4f 6153 tfrlemibxssdm 6286 tfr1onlembxssdm 6302 tfrcllembxssdm 6315 elixpsn 6692 ixpsnf1o 6693 mapsnen 6768 xpsnen 6778 xpassen 6787 xpf1o 6801 djulclr 7005 djurclr 7006 djulcl 7007 djurcl 7008 djulclb 7011 inl11 7021 djuss 7026 1stinl 7030 2ndinl 7031 1stinr 7032 2ndinr 7033 elreal 7760 ax1rid 7809 fseq1p1m1 10019 cnmpt21 12838 djucllem 13522 |
Copyright terms: Public domain | W3C validator |