| 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 | opabbidv.1 | . . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
| 2 | 1 | anbi2d 630 | . . . 4 ⊢ (𝜑 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒))) |
| 3 | 2 | 2exbidv 1924 | . . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒))) |
| 4 | 3 | abbidv 2808 | . 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒)}) |
| 5 | df-opab 5206 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)} | |
| 6 | df-opab 5206 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒)} | |
| 7 | 4, 5, 6 | 3eqtr4g 2802 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1540 ∃wex 1779 {cab 2714 〈cop 4632 {copab 5205 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-opab 5206 |
| This theorem is referenced by: opabbii 5210 mpteq12dva 5231 csbopab 5560 csbopabgALT 5561 csbmpt12 5562 xpeq1 5699 xpeq2 5706 opabbi2dv 5860 csbcnvgALT 5895 resopab2 6054 mptcnv 6159 cores 6269 xpco 6309 dffn5 6967 f1oiso2 7372 fvmptopab 7487 fvmptopabOLD 7488 f1ocnvd 7684 ofreq 7701 mptmpoopabbrd 8105 mptmpoopabbrdOLD 8106 mptmpoopabbrdOLDOLD 8108 bropopvvv 8115 bropfvvvv 8117 fnwelem 8156 sprmpod 8249 mpocurryd 8294 wemapwe 9737 ttrcleq 9749 xpcogend 15013 shftfval 15109 2shfti 15119 prdsval 17500 pwsle 17537 sectffval 17794 sectfval 17795 isfunc 17909 isfull 17957 isfth 17961 ipoval 18575 eqgfval 19194 eqg0subg 19214 dvdsrval 20361 dvdsrpropd 20416 ltbval 22061 opsrval 22064 lmfval 23240 xkocnv 23822 tgphaus 24125 isphtpc 25026 bcthlem1 25358 bcth 25363 dvcnp2 25955 dvmulbr 25975 dvcobr 25983 cmvth 26029 dvfsumle 26060 dvfsumlem2 26067 taylthlem2 26416 ulmval 26423 lgsquadlem3 27426 iscgrg 28520 legval 28592 ishlg 28610 perpln1 28718 perpln2 28719 isperp 28720 ishpg 28767 iscgra 28817 isinag 28846 isleag 28855 wksfval 29627 upgrtrls 29719 upgrspthswlk 29758 ajfval 30828 f1o3d 32637 f1od2 32732 mgcoval 32976 inftmrel 33187 isinftm 33188 erlval 33262 rlocval 33263 quslsm 33433 idlsrgval 33531 metidval 33889 faeval 34247 eulerpartlemgvv 34378 eulerpart 34384 afsval 34686 satf 35358 satfvsuc 35366 satfv1 35368 satf0suc 35381 sat1el2xp 35384 fmlasuc0 35389 bj-imdirvallem 37181 bj-imdirval2 37184 bj-imdirco 37191 bj-iminvval2 37195 cureq 37603 curf 37605 curunc 37609 fnopabeqd 37728 cosseq 38427 lcvfbr 39021 cmtfvalN 39211 cvrfval 39269 dicffval 41176 dicfval 41177 dicval 41178 prjspval 42613 prjspnerlem 42627 0prjspn 42638 dnwech 43060 aomclem8 43073 tfsconcatun 43350 tfsconcat0i 43358 tfsconcatrev 43361 rfovcnvfvd 44020 fsovrfovd 44022 dfafn5a 47172 sprsymrelfv 47481 sprsymrelfo 47484 upwlksfval 48051 upfval 48933 upfval2 48934 upfval3 48935 |
| Copyright terms: Public domain | W3C validator |