![]() |
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 2097 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sbequ2 1807 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid 195 |
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-12 1950 |
This theorem depends on definitions: df-bi 190 df-an 378 df-ex 1672 df-sb 1806 |
This theorem is referenced by: sbequ12r 2099 sbequ12a 2100 axc16ALT 2215 nfsb4t 2238 sbco2 2264 sb8 2273 sb8e 2274 sbal1 2309 clelab 2596 sbab 2598 cbvralf 2999 cbvralsv 3016 cbvrexsv 3017 cbvrab 3029 sbhypf 3081 mob2 3206 reu2 3214 reu6 3215 sbcralt 3328 sbcreu 3332 cbvreucsf 3383 cbvrabcsf 3384 csbif 3922 rabasiun 4273 cbvopab1 4466 cbvopab1s 4468 cbvmptf 4486 cbvmpt 4487 opelopabsb 4711 csbopab 4733 csbopabgALT 4734 opeliunxp 4891 ralxpf 4986 cbviota 5558 csbiota 5582 cbvriota 6280 csbriota 6282 onminex 6653 tfis 6700 findes 6742 abrexex2g 6789 opabex3d 6790 opabex3 6791 abrexex2 6793 dfoprab4f 6870 uzind4s 11242 ac6sf2 28302 esumcvg 28981 bj-sbab 31465 wl-sb8t 31950 wl-sbalnae 31962 wl-ax11-lem8 31986 sbcrexgOLD 35699 pm13.193 36832 opeliun2xp 40622 |
Copyright terms: Public domain | W3C validator |