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 form). (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
opabbidv | ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1909 | . 2 ⊢ Ⅎ𝑥𝜑 | |
2 | nfv 1909 | . 2 ⊢ Ⅎ𝑦𝜑 | |
3 | opabbidv.1 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
4 | 1, 2, 3 | opabbid 5122 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 208 = wceq 1531 {copab 5119 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-9 2118 ax-12 2170 ax-ext 2791 |
This theorem depends on definitions: df-bi 209 df-an 399 df-ex 1775 df-nf 1779 df-sb 2064 df-clab 2798 df-cleq 2812 df-opab 5120 |
This theorem is referenced by: opabbii 5124 csbopab 5433 csbopabgALT 5434 csbmpt12 5435 xpeq1 5562 xpeq2 5569 opabbi2dv 5713 csbcnvgALT 5748 resopab2 5897 mptcnv 5991 cores 6095 xpco 6133 dffn5 6717 f1oiso2 7097 fvmptopab 7201 f1ocnvd 7388 ofreq 7404 mptmpoopabbrd 7770 bropopvvv 7777 bropfvvvv 7779 fnwelem 7817 sprmpod 7882 mpocurryd 7927 wemapwe 9152 xpcogend 14326 shftfval 14421 2shfti 14431 prdsval 16720 pwsle 16757 sectffval 17012 sectfval 17013 isfunc 17126 isfull 17172 isfth 17176 ipoval 17756 eqgfval 18320 dvdsrval 19387 dvdsrpropd 19438 ltbval 20244 opsrval 20247 lmfval 21832 xkocnv 22414 tgphaus 22717 isphtpc 23590 bcthlem1 23919 bcth 23924 ulmval 24960 lgsquadlem3 25950 iscgrg 26290 legval 26362 ishlg 26380 perpln1 26488 perpln2 26489 isperp 26490 ishpg 26537 iscgra 26587 isinag 26616 isleag 26625 wksfval 27383 upgrtrls 27475 upgrspthswlk 27511 ajfval 28578 f1o3d 30364 f1od2 30449 inftmrel 30802 isinftm 30803 metidval 31123 faeval 31498 eulerpartlemgvv 31627 eulerpart 31633 afsval 31935 satf 32593 satfvsuc 32601 satfv1 32603 satf0suc 32616 sat1el2xp 32619 fmlasuc0 32624 bj-imdirval 34464 bj-imdirval2 34465 bj-imdirid 34467 cureq 34860 curf 34862 curunc 34866 fnopabeqd 34987 cosseq 35663 lcvfbr 36148 cmtfvalN 36338 cvrfval 36396 dicffval 38302 dicfval 38303 dicval 38304 prjspval 39244 prjspnval2 39258 0prjspn 39261 dnwech 39639 aomclem8 39652 rfovcnvfvd 40344 fsovrfovd 40346 dfafn5a 43350 sprsymrelfv 43647 sprsymrelfo 43650 upwlksfval 44001 |
Copyright terms: Public domain | W3C validator |