![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ralsng | Structured version Visualization version Unicode version |
Description: Substitution expressed in terms of quantification over a singleton. (Contributed by NM, 14-Dec-2005.) (Revised by Mario Carneiro, 23-Apr-2015.) |
Ref | Expression |
---|---|
ralsng.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ralsng |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ralsnsg 4015 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | ralsng.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | sbcieg 3312 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | bitrd 261 |
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 1680 ax-4 1693 ax-5 1769 ax-6 1816 ax-7 1862 ax-10 1926 ax-12 1944 ax-13 2102 ax-ext 2442 |
This theorem depends on definitions: df-bi 190 df-an 377 df-3an 993 df-tru 1458 df-ex 1675 df-nf 1679 df-sb 1809 df-clab 2449 df-cleq 2455 df-clel 2458 df-ral 2754 df-v 3059 df-sbc 3280 df-sn 3981 |
This theorem is referenced by: 2ralsng 4020 ralsn 4022 ralprg 4033 raltpg 4035 ralunsn 4200 iinxsng 4372 frirr 4830 posn 4922 frsn 4924 f12dfv 6197 ranksnb 8324 mgm1 16549 sgrp1 16583 mnd1 16626 mnd1OLD 16627 grp1 16807 cntzsnval 17027 abl1 17553 srgbinomlem4 17825 ring1 17879 mat1dimmul 19550 ufileu 20983 istrkg3ld 24558 cusgra1v 25238 cusgra2v 25239 dfconngra1 25448 1conngra 25452 wwlknext 25501 clwwlkn2 25552 wwlkext2clwwlk 25580 rusgrasn 25722 frgra1v 25775 poimirlem26 32011 poimirlem27 32012 poimirlem31 32016 dfconngr1 39929 1conngr 39935 zlidlring 40201 linds0 40531 snlindsntor 40537 lmod1 40558 |
Copyright terms: Public domain | W3C validator |