Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > opabbidv | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal ordered-pair class abstractions (deduction rule). (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
opabbidv | ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1830 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1830 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | opabbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 1, 2, 3 | opabbid 4647 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 {copab 4642 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-opab 4644 |
This theorem is referenced by: opabbii 4649 csbopab 4932 csbopabgALT 4933 csbmpt12 4934 xpeq1 5052 xpeq2 5053 opabbi2dv 5193 csbcnvgALT 5229 resopab2 5368 mptcnv 5453 cores 5555 xpco 5592 dffn5 6151 f1oiso2 6502 fvmptopab1 6594 f1ocnvd 6782 ofreq 6798 bropopvvv 7142 bropfvvvv 7144 fnwelem 7179 sprmpt2d 7237 mpt2curryd 7282 wemapwe 8477 xpcogend 13561 shftfval 13658 2shfti 13668 prdsval 15938 pwsle 15975 sectffval 16233 sectfval 16234 isfunc 16347 isfull 16393 isfth 16397 ipoval 16977 eqgfval 17465 dvdsrval 18468 dvdsrpropd 18519 ltbval 19292 opsrval 19295 lmfval 20846 xkocnv 21427 tgphaus 21730 isphtpc 22601 bcthlem1 22929 bcth 22934 ulmval 23938 lgsquadlem3 24907 iscgrg 25207 legval 25279 ishlg 25297 perpln1 25405 perpln2 25406 isperp 25407 ishpg 25451 iscgra 25501 isinag 25529 isleag 25533 wlks 26047 wlkcompim 26054 wlkelwrd 26058 wlkon 26061 trls 26066 trlon 26070 pths 26096 spths 26097 pthon 26105 spthon 26112 clwlk 26281 clwlkcompim 26292 iseupa 26492 ajfval 27048 f1o3d 28813 f1od2 28887 inftmrel 29065 isinftm 29066 metidval 29261 faeval 29636 eulerpartlemgvv 29765 eulerpart 29771 afsval 30002 cureq 32555 curf 32557 curunc 32561 fnopabeqd 32684 lcvfbr 33325 cmtfvalN 33515 cvrfval 33573 dicffval 35481 dicfval 35482 dicval 35483 dnwech 36636 aomclem8 36649 rfovcnvfvd 37321 fsovrfovd 37323 dfafn5a 39889 mptmpt2opabbrd 40335 1wlksfval 40811 wlksfval 40812 upgrtrls 40909 upgrspths1wlk 40944 |
Copyright terms: Public domain | W3C validator |