![]() |
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 1883 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1883 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | opabbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 1, 2, 3 | opabbid 4748 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1523 {copab 4745 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1762 ax-4 1777 ax-5 1879 ax-6 1945 ax-7 1981 ax-9 2039 ax-10 2059 ax-11 2074 ax-12 2087 ax-13 2282 ax-ext 2631 |
This theorem depends on definitions: df-bi 197 df-or 384 df-an 385 df-tru 1526 df-ex 1745 df-nf 1750 df-sb 1938 df-clab 2638 df-cleq 2644 df-clel 2647 df-opab 4746 |
This theorem is referenced by: opabbii 4750 csbopab 5037 csbopabgALT 5038 csbmpt12 5039 xpeq1 5157 xpeq2 5163 opabbi2dv 5304 csbcnvgALT 5339 resopab2 5483 mptcnv 5569 cores 5676 xpco 5713 dffn5 6280 f1oiso2 6642 fvmptopab 6739 f1ocnvd 6926 ofreq 6942 mptmpt2opabbrd 7293 bropopvvv 7300 bropfvvvv 7302 fnwelem 7337 sprmpt2d 7395 mpt2curryd 7440 wemapwe 8632 xpcogend 13759 shftfval 13854 2shfti 13864 prdsval 16162 pwsle 16199 sectffval 16457 sectfval 16458 isfunc 16571 isfull 16617 isfth 16621 ipoval 17201 eqgfval 17689 dvdsrval 18691 dvdsrpropd 18742 ltbval 19519 opsrval 19522 lmfval 21084 xkocnv 21665 tgphaus 21967 isphtpc 22840 bcthlem1 23167 bcth 23172 ulmval 24179 lgsquadlem3 25152 iscgrg 25452 legval 25524 ishlg 25542 perpln1 25650 perpln2 25651 isperp 25652 ishpg 25696 iscgra 25746 isinag 25774 isleag 25778 wksfval 26561 upgrtrls 26654 upgrspthswlk 26690 ajfval 27792 f1o3d 29559 f1od2 29627 inftmrel 29862 isinftm 29863 metidval 30061 faeval 30437 eulerpartlemgvv 30566 eulerpart 30572 afsval 30877 cureq 33515 curf 33517 curunc 33521 fnopabeqd 33644 cosseq 34321 lcvfbr 34625 cmtfvalN 34815 cvrfval 34873 dicffval 36780 dicfval 36781 dicval 36782 dnwech 37935 aomclem8 37948 rfovcnvfvd 38618 fsovrfovd 38620 dfafn5a 41561 upwlksfval 42041 sprsymrelfv 42069 sprsymrelfo 42072 |
Copyright terms: Public domain | W3C validator |