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 3278 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 195 = wceq 1475 ∈ wcel 1977 ∀wral 2896 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 |
This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-v 3175 |
This theorem is referenced by: elinti 4420 trss 4689 fvn0ssdmfun 6258 dff3 6280 2fvcoidd 6452 ofrval 6805 limsuc 6941 limuni3 6944 frxp 7174 wfrdmcl 7310 smo11 7348 odi 7546 supub 8248 suplub 8249 elirrv 8387 dfom3 8427 noinfep 8440 oemapvali 8464 tcrank 8630 infxpenlem 8719 alephle 8794 dfac5lem5 8833 dfac2 8836 cofsmo 8974 coftr 8978 infpssrlem4 9011 isf34lem6 9085 axcc2lem 9141 domtriomlem 9147 axdc2lem 9153 axdc3lem2 9156 axdc4lem 9160 ac5b 9183 zorn2lem2 9202 zorn2lem6 9206 pwcfsdom 9284 inar1 9476 grupw 9496 grupr 9498 gruurn 9499 grothpw 9527 grothpwex 9528 axgroth6 9529 grothomex 9530 nqereu 9630 supsrlem 9811 axpre-sup 9869 dedekind 10079 dedekindle 10080 supmullem1 10870 supmul 10872 peano5nni 10900 dfnn2 10910 peano5uzi 11342 zindd 11354 1arith 15469 ramcl 15571 clatleglb 16949 pslem 17029 cygabl 18115 eqcoe1ply1eq 19488 psgndiflemA 19766 mvmumamul1 20179 smadiadetlem0 20286 chpscmat 20466 basis2 20566 tg2 20580 clsndisj 20689 cnpimaex 20870 t1sncld 20940 regsep 20948 nrmsep3 20969 cmpsub 21013 2ndc1stc 21064 refssex 21124 ptfinfin 21132 txcnpi 21221 txcmplem1 21254 tx1stc 21263 filss 21467 ufilss 21519 fclsopni 21629 fclsrest 21638 alexsubb 21660 alexsubALTlem2 21662 alexsubALTlem4 21664 ghmcnp 21728 qustgplem 21734 mopni 22107 metrest 22139 metcnpi 22159 metcnpi2 22160 cfilucfil 22174 nmolb 22331 nmoleub2lem2 22724 ovoliunlem1 23077 ovolicc2lem3 23094 mblsplit 23107 fta1b 23733 plycj 23837 mtest 23962 lgamgulmlem1 24555 sqfpc 24663 ostth2lem2 25123 ostth3 25127 vdiscusgra 26448 rusgranumwwlkl1 26473 usgn0fidegnn0 26556 numclwwlk1 26625 lpni 26722 nvz 26908 ubthlem2 27111 chcompl 27483 ocin 27539 hmopidmchi 28394 dmdmd 28543 dmdbr5 28551 mdsl1i 28564 sigaclci 29522 bnj23 30038 kur14lem9 30450 sconpht 30465 cvmsdisj 30506 untelirr 30839 untsucf 30841 dfon2lem4 30935 dfon2lem6 30937 dfon2lem7 30938 dfon2lem8 30939 dfon2 30941 frrlem5e 31032 sltval2 31053 fwddifnp1 31442 poimirlem18 32597 poimirlem21 32600 heibor1lem 32778 heiborlem4 32783 heiborlem6 32785 atlex 33621 psubspi 34051 elpcliN 34197 ldilval 34417 trlord 34875 tendotp 35067 hdmapval2 36142 pwelg 36884 gneispace0nelrn2 37459 gneispaceel2 37462 gneispacess2 37464 stoweid 38956 iccpartltu 39963 iccpartgtl 39964 iccpartleu 39966 iccpartgel 39967 nbgrnself2 40585 vdiscusgr 40747 rusgrnumwrdl2 40786 ewlkinedg 40806 av-numclwwlk1 41528 ssdifsn 42228 |
Copyright terms: Public domain | W3C validator |