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 3305 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1483 ∈ wcel 1990 ∀wral 2912 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 |
This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-v 3202 |
This theorem is referenced by: ssdifsn 4318 elinti 4485 trss 4761 fvn0ssdmfun 6350 dff3 6372 2fvcoidd 6552 ofrval 6907 limsuc 7049 limuni3 7052 frxp 7287 wfrdmcl 7423 smo11 7461 odi 7659 supub 8365 suplub 8366 elirrv 8504 dfom3 8544 noinfep 8557 oemapvali 8581 tcrank 8747 infxpenlem 8836 alephle 8911 dfac5lem5 8950 dfac2 8953 cofsmo 9091 coftr 9095 infpssrlem4 9128 isf34lem6 9202 axcc2lem 9258 domtriomlem 9264 axdc2lem 9270 axdc3lem2 9273 axdc4lem 9277 ac5b 9300 zorn2lem2 9319 zorn2lem6 9323 pwcfsdom 9405 inar1 9597 grupw 9617 grupr 9619 gruurn 9620 grothpw 9648 grothpwex 9649 axgroth6 9650 grothomex 9651 nqereu 9751 supsrlem 9932 axpre-sup 9990 dedekind 10200 dedekindle 10201 supmullem1 10993 supmul 10995 peano5nni 11023 dfnn2 11033 peano5uzi 11466 zindd 11478 1arith 15631 ramcl 15733 clatleglb 17126 pslem 17206 cygabl 18292 eqcoe1ply1eq 19667 psgndiflemA 19947 mvmumamul1 20360 smadiadetlem0 20467 chpscmat 20647 basis2 20755 tg2 20769 clsndisj 20879 cnpimaex 21060 t1sncld 21130 regsep 21138 nrmsep3 21159 cmpsub 21203 2ndc1stc 21254 refssex 21314 ptfinfin 21322 txcnpi 21411 txcmplem1 21444 tx1stc 21453 filss 21657 ufilss 21709 fclsopni 21819 fclsrest 21828 alexsubb 21850 alexsubALTlem2 21852 alexsubALTlem4 21854 ghmcnp 21918 qustgplem 21924 mopni 22297 metrest 22329 metcnpi 22349 metcnpi2 22350 cfilucfil 22364 nmolb 22521 nmoleub2lem2 22916 ovoliunlem1 23270 ovolicc2lem3 23287 mblsplit 23300 fta1b 23929 plycj 24033 mtest 24158 lgamgulmlem1 24755 sqfpc 24863 ostth2lem2 25323 ostth3 25327 nbgrnself2 26259 vdiscusgr 26427 rusgrnumwrdl2 26482 ewlkinedg 26500 numclwwlk1 27231 l2p 27331 lpni 27332 nvz 27524 ubthlem2 27727 chcompl 28099 ocin 28155 hmopidmchi 29010 dmdmd 29159 dmdbr5 29167 mdsl1i 29180 sigaclci 30195 bnj23 30784 kur14lem9 31196 sconnpht 31211 cvmsdisj 31252 untelirr 31585 untsucf 31587 dfon2lem4 31691 dfon2lem6 31693 dfon2lem7 31694 dfon2lem8 31695 dfon2 31697 frrlem5e 31788 sltval2 31809 fwddifnp1 32272 poimirlem18 33427 poimirlem21 33430 heibor1lem 33608 heiborlem4 33613 heiborlem6 33615 atlex 34603 psubspi 35033 elpcliN 35179 ldilval 35399 trlord 35857 tendotp 36049 hdmapval2 37124 pwelg 37865 gneispace0nelrn2 38439 gneispaceel2 38442 gneispacess2 38444 stoweid 40280 iccpartltu 41361 iccpartgtl 41362 iccpartleu 41364 iccpartgel 41365 |
Copyright terms: Public domain | W3C validator |