![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opabbii | GIF version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 | ⊢ (𝜑 ↔ 𝜓) |
Ref | Expression |
---|---|
opabbii | ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2100 | . 2 ⊢ 𝑧 = 𝑧 | |
2 | opabbii.1 | . . . 4 ⊢ (𝜑 ↔ 𝜓) | |
3 | 2 | a1i 9 | . . 3 ⊢ (𝑧 = 𝑧 → (𝜑 ↔ 𝜓)) |
4 | 3 | opabbidv 3934 | . 2 ⊢ (𝑧 = 𝑧 → {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓}) |
5 | 1, 4 | ax-mp 7 | 1 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜑} = {〈𝑥, 𝑦〉 ∣ 𝜓} |
Colors of variables: wff set class |
Syntax hints: ↔ wb 104 = wceq 1299 {copab 3928 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-5 1391 ax-7 1392 ax-gen 1393 ax-ie1 1437 ax-ie2 1438 ax-8 1450 ax-11 1452 ax-4 1455 ax-17 1474 ax-i9 1478 ax-ial 1482 ax-i5r 1483 ax-ext 2082 |
This theorem depends on definitions: df-bi 116 df-tru 1302 df-nf 1405 df-sb 1704 df-clab 2087 df-cleq 2093 df-opab 3930 |
This theorem is referenced by: mptv 3965 fconstmpt 4524 xpundi 4533 xpundir 4534 inxp 4611 cnvco 4662 resopab 4799 opabresid 4808 cnvi 4879 cnvun 4880 cnvin 4882 cnvxp 4893 cnvcnv3 4924 coundi 4976 coundir 4977 mptun 5190 fvopab6 5449 cbvoprab1 5775 cbvoprab12 5777 dmoprabss 5785 mpomptx 5794 resoprab 5799 ov6g 5840 dfoprab3s 6018 dfoprab3 6019 dfoprab4 6020 mapsncnv 6519 xpcomco 6649 dmaddpq 7088 dmmulpq 7089 recmulnqg 7100 enq0enq 7140 ltrelxr 7697 ltxr 9403 shftidt2 10445 lmfval 12143 lmbr 12163 cnmptid 12231 |
Copyright terms: Public domain | W3C validator |