![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > opabbii | Structured version Visualization version Unicode version |
Description: Equivalent wff's yield equal class abstractions. (Contributed by NM, 15-May-1995.) |
Ref | Expression |
---|---|
opabbii.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
opabbii |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqid 2471 |
. 2
![]() ![]() ![]() ![]() | |
2 | opabbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | opabbidv 4459 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | ax-mp 5 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 |
This theorem depends on definitions: df-bi 190 df-an 378 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-clab 2458 df-cleq 2464 df-clel 2467 df-opab 4455 |
This theorem is referenced by: mptv 4489 2rbropap 4742 dfid4 4756 fconstmpt 4883 xpundi 4892 xpundir 4893 inxp 4972 csbcnv 5023 cnvco 5025 resopab 5157 opabresid 5164 cnvi 5246 cnvun 5247 cnvxp 5260 cnvcnv3 5291 coundi 5343 coundir 5344 mptun 5719 fvopab6 5990 fmptsng 6101 fmptsnd 6102 fvmptopab2 6352 cbvoprab1 6382 cbvoprab12 6384 dmoprabss 6397 mpt2mptx 6406 resoprab 6411 elrnmpt2res 6429 ov6g 6453 1st2val 6838 2nd2val 6839 dfoprab3s 6867 dfoprab3 6868 dfoprab4 6869 fsplit 6920 mapsncnv 7536 xpcomco 7680 marypha2lem2 7968 oemapso 8205 leweon 8460 r0weon 8461 compsscnv 8819 fpwwe 9089 ltrelxr 9713 ltxrlt 9722 ltxr 11438 shftidt2 13221 prdsle 15438 prdsless 15439 prdsleval 15453 dfiso2 15755 joindm 16327 meetdm 16341 gaorb 17039 efgcpbllema 17482 frgpuplem 17500 ltbval 18772 ltbwe 18773 opsrle 18776 opsrtoslem1 18784 opsrtoslem2 18785 dvdsrzring 19129 pjfval2 19349 lmfval 20325 lmbr 20351 cnmptid 20753 lgsquadlem3 24363 perpln1 24834 outpasch 24876 ishpg 24880 axcontlem2 25074 wlks 25326 trls 25345 dfconngra1 25478 dfadj2 27619 dmadjss 27621 cnvadj 27626 mpt2mptxf 28355 fneer 31080 bj-dfmpt2a 31700 bj-mpt2mptALT 31701 opropabco 32114 cmtfvalN 32847 cmtvalN 32848 cvrfval 32905 cvrval 32906 dicval2 34818 fgraphopab 36158 fgraphxp 36159 opabn1stprc 39153 opabbrfex0d 39176 opabbrfexd 39178 mptmpt2opabbrd 39180 1wlksfval 39813 wlksfval 39814 wlkson 39854 xpsnopab 40273 mpt2mptx2 40624 |
Copyright terms: Public domain | W3C validator |