![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspccv | Structured version Visualization version GIF version |
Description: Restricted specialization, using implicit substitution. (Contributed by NM, 2-Feb-2006.) |
Ref | Expression |
---|---|
rspcv.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspccv | ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspcv.1 | . . 3 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜓)) | |
2 | 1 | rspcv 3528 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 198 = wceq 1507 ∈ wcel 2048 ∀wral 3085 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1964 ax-8 2050 ax-9 2057 ax-10 2077 ax-11 2091 ax-12 2104 ax-ext 2747 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2014 df-clab 2756 df-cleq 2768 df-clel 2843 df-nfc 2915 df-ral 3090 df-v 3414 |
This theorem is referenced by: elinti 4756 trss 5037 fvn0ssdmfun 6665 dff3 6687 2fvcoidd 6876 ofrval 7235 limsuc 7378 limuni3 7381 frxp 7622 wfrdmcl 7764 smo11 7802 odi 8002 supub 8714 suplub 8715 elirrv 8851 dfom3 8900 noinfep 8913 tcrank 9103 alephle 9304 dfac5lem5 9343 dfac2b 9346 cofsmo 9485 coftr 9489 infpssrlem4 9522 isf34lem6 9596 axcc2lem 9652 domtriomlem 9658 axdc2lem 9664 axdc3lem2 9667 axdc4lem 9671 ac5b 9694 zorn2lem2 9713 zorn2lem6 9717 pwcfsdom 9799 inar1 9991 grupw 10011 grupr 10013 gruurn 10014 grothpw 10042 grothpwex 10043 axgroth6 10044 grothomex 10045 nqereu 10145 supsrlem 10327 axpre-sup 10385 dedekind 10599 dedekindle 10600 supmullem1 11408 supmul 11410 peano5nni 11438 dfnn2 11450 peano5uzi 11881 zindd 11893 lcmfdvds 15836 lcmfunsn 15838 1arith 16113 ramcl 16215 clatleglb 17588 pslem 17668 cygabl 18759 eqcoe1ply1eq 20162 psgndiflemA 20441 mvmumamul1 20861 smadiadetlem0 20968 chpscmat 21148 basis2 21257 tg2 21271 clsndisj 21381 cnpimaex 21562 t1sncld 21632 regsep 21640 nrmsep3 21661 cmpsub 21706 2ndc1stc 21757 refssex 21817 ptfinfin 21825 txcnpi 21914 txcmplem1 21947 tx1stc 21956 filss 22159 ufilss 22211 fclsopni 22321 fclsrest 22330 alexsubb 22352 alexsubALTlem2 22354 alexsubALTlem4 22356 ghmcnp 22420 qustgplem 22426 mopni 22799 metrest 22831 metcnpi 22851 metcnpi2 22852 nmolb 23023 nmoleub2lem2 23417 ovoliunlem1 23800 ovolicc2lem3 23817 mblsplit 23830 fta1b 24460 plycj 24564 lgamgulmlem1 25302 sqfpc 25410 ostth2lem2 25906 ostth3 25910 vdiscusgr 27010 0vtxrusgr 27056 rusgrnumwrdl2 27065 ewlkinedg 27083 eupthseg 27729 upgreupthseg 27732 numclwwlk1 27903 l2p 28027 lpni 28028 nvz 28217 chcompl 28792 ocin 28848 hmopidmchi 29703 dmdmd 29852 dmdbr5 29860 mdsl1i 29873 sigaclci 31027 bnj23 31627 kur14lem9 32036 sconnpht 32051 cvmsdisj 32092 untelirr 32424 untsucf 32426 dfon2lem4 32521 dfon2lem6 32523 dfon2lem7 32524 dfon2lem8 32525 dfon2 32527 sltval2 32654 fwddifnp1 33117 domalom 34091 pibt2 34104 poimirlem18 34329 poimirlem21 34332 heibor1lem 34507 heiborlem4 34512 heiborlem6 34514 atlex 35875 psubspi 36306 elpcliN 36452 ldilval 36672 trlord 37128 tendotp 37320 hdmapval2 38391 pwelg 39259 gneispace0nelrn2 39832 gneispaceel2 39835 gneispacess2 39837 stoweid 41758 iccpartimp 42928 iccpartltu 42936 iccpartgtl 42937 iccpartleu 42939 iccpartgel 42940 isomushgr 43333 isomuspgrlem1 43334 isomuspgr 43341 isomgrtrlem 43345 |
Copyright terms: Public domain | W3C validator |