![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > sbequ12 | Structured version Visualization version Unicode version |
Description: An equality theorem for substitution. (Contributed by NM, 14-May-1993.) |
Ref | Expression |
---|---|
sbequ12 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sbequ1 2082 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sbequ2 1799 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid 194 |
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 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-12 1933 |
This theorem depends on definitions: df-bi 189 df-an 373 df-ex 1664 df-sb 1798 |
This theorem is referenced by: sbequ12r 2084 sbequ12a 2085 axc16ALT 2195 nfsb4t 2218 sbco2 2244 sb8 2253 sb8e 2254 sbal1 2289 clelab 2576 sbab 2578 cbvralf 3013 cbvralsv 3030 cbvrexsv 3031 cbvrab 3043 sbhypf 3095 mob2 3218 reu2 3226 reu6 3227 sbcralt 3340 sbcreu 3344 cbvreucsf 3397 cbvrabcsf 3398 csbif 3931 rabasiun 4282 cbvopab1 4473 cbvopab1s 4475 cbvmptf 4493 cbvmpt 4494 opelopabsb 4711 csbopab 4733 csbopabgALT 4734 opeliunxp 4886 ralxpf 4981 cbviota 5551 csbiota 5575 cbvriota 6262 csbriota 6264 onminex 6634 tfis 6681 findes 6723 abrexex2g 6770 opabex3d 6771 opabex3 6772 abrexex2 6774 dfoprab4f 6851 uzind4s 11219 ac6sf2 28226 esumcvg 28907 bj-sbab 31399 wl-sb8t 31880 wl-sbalnae 31892 wl-ax11-lem8 31922 sbcrexgOLD 35628 pm13.193 36762 opeliun2xp 40167 |
Copyright terms: Public domain | W3C validator |