![]() |
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 628 | . . . 4 ⊢ (𝜑 → ((𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ (𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒))) |
3 | 2 | 2exbidv 1919 | . . 3 ⊢ (𝜑 → (∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓) ↔ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒))) |
4 | 3 | abbidv 2794 | . 2 ⊢ (𝜑 → {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒)}) |
5 | df-opab 5215 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜓} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜓)} | |
6 | df-opab 5215 | . 2 ⊢ {〈𝑥, 𝑦〉 ∣ 𝜒} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = 〈𝑥, 𝑦〉 ∧ 𝜒)} | |
7 | 4, 5, 6 | 3eqtr4g 2790 | 1 ⊢ (𝜑 → {〈𝑥, 𝑦〉 ∣ 𝜓} = {〈𝑥, 𝑦〉 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1533 ∃wex 1773 {cab 2702 〈cop 4638 {copab 5214 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-opab 5215 |
This theorem is referenced by: opabbii 5219 mpteq12dva 5241 csbopab 5560 csbopabgALT 5561 csbmpt12 5562 xpeq1 5695 xpeq2 5702 opabbi2dv 5855 csbcnvgALT 5890 resopab2 6044 mptcnv 6150 cores 6259 xpco 6299 dffn5 6960 f1oiso2 7363 fvmptopab 7478 fvmptopabOLD 7479 f1ocnvd 7676 ofreq 7693 mptmpoopabbrd 8093 mptmpoopabbrdOLD 8094 mptmpoopabbrdOLDOLD 8096 bropopvvv 8103 bropfvvvv 8105 fnwelem 8144 sprmpod 8238 mpocurryd 8283 wemapwe 9736 ttrcleq 9748 xpcogend 14974 shftfval 15070 2shfti 15080 prdsval 17465 pwsle 17502 sectffval 17761 sectfval 17762 isfunc 17878 isfull 17927 isfth 17931 ipoval 18550 eqgfval 19165 eqg0subg 19185 dvdsrval 20338 dvdsrpropd 20393 ltbval 22042 opsrval 22045 lmfval 23219 xkocnv 23801 tgphaus 24104 isphtpc 25003 bcthlem1 25335 bcth 25340 dvcnp2 25932 dvmulbr 25952 dvcobr 25960 cmvth 26006 dvfsumle 26037 dvfsumlem2 26044 taylthlem2 26394 ulmval 26401 lgsquadlem3 27403 iscgrg 28431 legval 28503 ishlg 28521 perpln1 28629 perpln2 28630 isperp 28631 ishpg 28678 iscgra 28728 isinag 28757 isleag 28766 wksfval 29538 upgrtrls 29630 upgrspthswlk 29667 ajfval 30734 f1o3d 32535 f1od2 32626 mgcoval 32844 inftmrel 33022 isinftm 33023 erlval 33090 rlocval 33091 quslsm 33257 idlsrgval 33355 metidval 33661 faeval 34035 eulerpartlemgvv 34166 eulerpart 34172 afsval 34473 satf 35133 satfvsuc 35141 satfv1 35143 satf0suc 35156 sat1el2xp 35159 fmlasuc0 35164 bj-imdirvallem 36835 bj-imdirval2 36838 bj-imdirco 36845 bj-iminvval2 36849 cureq 37245 curf 37247 curunc 37251 fnopabeqd 37370 cosseq 38072 lcvfbr 38666 cmtfvalN 38856 cvrfval 38914 dicffval 40821 dicfval 40822 dicval 40823 prjspval 42194 prjspnerlem 42208 0prjspn 42219 dnwech 42646 aomclem8 42659 tfsconcatun 42940 tfsconcat0i 42948 tfsconcatrev 42951 rfovcnvfvd 43611 fsovrfovd 43613 dfafn5a 46710 sprsymrelfv 47003 sprsymrelfo 47006 upwlksfval 47449 |
Copyright terms: Public domain | W3C validator |