![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > abbidv | Structured version Visualization version GIF version |
Description: Equivalent wff's yield equal class abstractions (deduction form). (Contributed by NM, 10-Aug-1993.) Avoid ax-12 2163, based on an idea of Steven Nguyen. (Revised by Wolf Lammen, 6-May-2023.) |
Ref | Expression |
---|---|
abbidv.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Ref | Expression |
---|---|
abbidv | ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | abbidv.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 1 | sbbidv 2020 | . 2 ⊢ (𝜑 → ([𝑦 / 𝑥]𝜓 ↔ [𝑦 / 𝑥]𝜒)) |
3 | 2 | abbilem 2903 | 1 ⊢ (𝜑 → {𝑥 ∣ 𝜓} = {𝑥 ∣ 𝜒}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1601 {cab 2763 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-ex 1824 df-sb 2012 df-clab 2764 df-cleq 2770 |
This theorem is referenced by: abbii 2908 rabbidva2 3383 cdeqab 3642 sbceqbid 3659 csbeq1 3754 csbeq2 3755 csbprc 4206 sbcel12 4208 sbceqg 4209 csbeq2d 4216 csbnestgf 4221 pweq 4382 sneq 4408 csbsng 4475 unieq 4681 csbuni 4703 inteq 4715 iineq1 4770 iineq2 4773 dfiin2g 4788 iinrab 4817 iinxprg 4836 opabbid 4953 imasng 5743 iotaeq 6109 iotabi 6110 dfimafn 6507 fnsnfv 6520 fliftf 6839 oprabbid 6987 wrecseq123 7692 rdglim2 7813 qseq1 8080 qseq2 8081 qsinxp 8108 mapvalg 8152 ixpsnval 8199 ixpeq1 8207 fival 8608 tcvalg 8913 karden 9057 acneq 9201 infmap2 9377 cfval 9406 cflim3 9421 axdclem 9678 axdc 9680 rankcf 9936 genpv 10158 negfi 11330 supadd 11350 hashf1lem2 13560 hashf1 13561 hashfac 13562 csbwrdg 13639 cshimadifsn 13986 cshimadifsn0 13987 cleq1 14137 dfrtrcl2 14215 shftlem 14221 shftfib 14225 vdwlem6 16105 cshwsiun 16216 lubfval 17375 glbfval 17388 eqglact 18040 isghm 18055 symgval 18193 sylow1lem2 18409 sylow3lem1 18437 efgval 18525 dmdprd 18795 ixpsnbasval 19617 aspval2 19755 ressmplbas2 19863 cssval 20436 tgval 21178 clsval2 21273 lpfval 21361 lpval 21362 islocfin 21740 ptval 21793 hauspwpwf1 22210 ptcmplem2 22276 snclseqg 22338 ustval 22425 itg2val 23943 limcfval 24084 plyval 24397 isismt 25902 nb3grprlem1 26745 vtxdun 26846 rgrx0ndm 26958 ewlksfval 26966 wwlksnfiOLD 27296 rusgrnumwwlkb0 27368 eclclwwlkn1 27490 avril1 27911 nmoofval 28206 nmooval 28207 nmoo0 28235 nmopval 29304 nmfnval 29324 iunrdx 29961 disjabrex 29975 disjabrexf 29976 dfimafnf 30018 curry2ima 30069 pstmval 30544 pstmfval 30545 sigaval 30779 measval 30867 orvcval 31126 bnj956 31454 bnj18eq1 31604 bnj1318 31700 derangval 31756 mclsval 32067 dfrdg2 32297 dfrdg3 32298 frecseq123 32374 altxpeq1 32677 altxpeq2 32678 bj-snsetex 33531 bj-sngleq 33535 bj-projeq 33560 bj-projval 33564 bj-imafv 33736 csbwrecsg 33776 csboprabg 33779 finxpeq1 33825 finxpeq2 33826 csbfinxpg 33827 finxpreclem6 33835 ptrest 34043 poimirlem26 34070 poimirlem27 34071 poimirlem28 34072 mblfinlem3 34083 cnambfre 34092 itg2addnc 34098 areacirclem5 34138 sdclem2 34171 sdc 34173 ismtyval 34232 elghomlem1OLD 34317 iineq12f 34604 eccnvepres 34686 lfl1dim 35284 ldual1dim 35329 glbconxN 35541 lineset 35901 pointsetN 35904 psubspset 35907 pmapglb2xN 35935 polval2N 36069 psubclsetN 36099 lautset 36245 pautsetN 36261 tendofset 36921 tendoset 36922 dva1dim 37148 dia1dim2 37225 dib1dim2 37331 diclspsn 37357 dih1dimatlem 37492 dihglb2 37505 hdmap1ffval 37958 hdmapffval 37989 hgmapffval 38048 eldiophb 38294 eldioph 38295 diophrw 38296 eldioph2 38299 eldioph2b 38300 eldioph3 38303 diophin 38310 diophun 38311 diophrex 38313 rexrabdioph 38332 rmxypairf1o 38449 hbtlem1 38666 hbtlem7 38668 nzss 39486 dropab1 39619 dropab2 39620 supsubc 40491 dfaimafn 42220 dfatsnafv2 42307 rnfdmpr 42336 f1oresf1o 42345 f1oresf1o2 42346 fargshiftfo 42424 sprval 42432 sprvalpw 42433 prprval 42467 prprvalpw 42468 prprspr2 42471 setrecseq 43551 |
Copyright terms: Public domain | W3C validator |