![]() |
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 2450 |
. 2
![]() ![]() ![]() ![]() | |
2 | opabbii.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | a1i 11 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | opabbidv 4465 |
. 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 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 |
This theorem depends on definitions: df-bi 189 df-an 373 df-tru 1446 df-ex 1663 df-nf 1667 df-sb 1797 df-clab 2437 df-cleq 2443 df-clel 2446 df-opab 4461 |
This theorem is referenced by: mptv 4495 dfid4 4750 fconstmpt 4877 xpundi 4886 xpundir 4887 inxp 4966 csbcnv 5017 cnvco 5019 resopab 5150 opabresid 5157 cnvi 5239 cnvun 5240 cnvxp 5253 cnvcnv3 5284 coundi 5335 coundir 5336 mptun 5707 fvopab6 5973 fmptsng 6083 fmptsnd 6084 cbvoprab1 6360 cbvoprab12 6362 dmoprabss 6375 mpt2mptx 6384 resoprab 6389 elrnmpt2res 6407 ov6g 6431 1st2val 6816 2nd2val 6817 dfoprab3s 6845 dfoprab3 6846 dfoprab4 6847 fsplit 6898 mapsncnv 7515 xpcomco 7659 marypha2lem2 7947 oemapso 8184 leweon 8439 r0weon 8440 compsscnv 8798 fpwwe 9068 ltrelxr 9692 ltxrlt 9701 ltxr 11412 shftidt2 13137 prdsle 15353 prdsless 15354 prdsleval 15368 dfiso2 15670 joindm 16242 meetdm 16256 gaorb 16954 efgcpbllema 17397 frgpuplem 17415 ltbval 18688 ltbwe 18689 opsrle 18692 opsrtoslem1 18700 opsrtoslem2 18701 dvdsrzring 19045 pjfval2 19265 lmfval 20241 lmbr 20267 cnmptid 20669 lgsquadlem3 24277 perpln1 24748 outpasch 24790 ishpg 24794 axcontlem2 24988 wlks 25240 trls 25259 dfconngra1 25392 dfadj2 27531 dmadjss 27533 cnvadj 27538 mpt2mptxf 28273 fneer 31002 bj-dfmpt2a 31623 bj-mpt2mptALT 31624 opropabco 32043 cmtfvalN 32770 cmtvalN 32771 cvrfval 32828 cvrval 32829 dicval2 34741 fgraphopab 36081 fgraphxp 36082 opabn1stprc 39001 1wlksfval 39609 wlksfval 39610 xpsnopab 39752 mpt2mptx2 40103 |
Copyright terms: Public domain | W3C validator |