![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > opabbidv | GIF version |
Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction form). (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
opabbidv | ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1539 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1539 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | opabbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 1, 2, 3 | opabbid 4083 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 = wceq 1364 {copab 4078 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-11 1517 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-tru 1367 df-nf 1472 df-sb 1774 df-clab 2176 df-cleq 2182 df-opab 4080 |
This theorem is referenced by: opabbii 4085 csbopabg 4096 xpeq1 4658 xpeq2 4659 opabbi2dv 4794 csbcnvg 4829 resopab2 4972 mptcnv 5049 cores 5150 xpcom 5193 dffn5im 5581 f1oiso2 5848 f1ocnvd 6095 ofreq 6109 f1od2 6259 shftfvalg 10858 shftfval 10861 2shfti 10871 prdsex 12771 releqgg 13156 eqgex 13157 eqgfval 13158 reldvdsrsrg 13439 dvdsrvald 13440 dvdsrpropdg 13494 aprval 13595 aprap 13599 lmfval 14144 |
Copyright terms: Public domain | W3C validator |