![]() |
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 3456 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 196 = wceq 1631 ∈ wcel 2145 ∀wral 3061 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1870 ax-4 1885 ax-5 1991 ax-6 2057 ax-7 2093 ax-9 2154 ax-10 2174 ax-11 2190 ax-12 2203 ax-13 2408 ax-ext 2751 |
This theorem depends on definitions: df-bi 197 df-an 383 df-or 835 df-tru 1634 df-ex 1853 df-nf 1858 df-sb 2050 df-clab 2758 df-cleq 2764 df-clel 2767 df-nfc 2902 df-ral 3066 df-v 3353 |
This theorem is referenced by: ssdifsnOLD 4455 elinti 4620 trss 4895 fvn0ssdmfun 6493 dff3 6515 2fvcoidd 6695 ofrval 7054 limsuc 7196 limuni3 7199 frxp 7438 wfrdmcl 7576 smo11 7614 odi 7813 supub 8521 suplub 8522 elirrv 8657 dfom3 8708 noinfep 8721 tcrank 8911 alephle 9111 dfac5lem5 9150 dfac2b 9153 dfac2OLD 9155 cofsmo 9293 coftr 9297 infpssrlem4 9330 isf34lem6 9404 axcc2lem 9460 domtriomlem 9466 axdc2lem 9472 axdc3lem2 9475 axdc4lem 9479 ac5b 9502 zorn2lem2 9521 zorn2lem6 9525 pwcfsdom 9607 inar1 9799 grupw 9819 grupr 9821 gruurn 9822 grothpw 9850 grothpwex 9851 axgroth6 9852 grothomex 9853 nqereu 9953 supsrlem 10134 axpre-sup 10192 dedekind 10402 dedekindle 10403 supmullem1 11195 supmul 11197 peano5nni 11225 dfnn2 11235 peano5uzi 11668 zindd 11680 1arith 15838 ramcl 15940 clatleglb 17334 pslem 17414 cygabl 18499 eqcoe1ply1eq 19882 psgndiflemA 20163 mvmumamul1 20578 smadiadetlem0 20686 chpscmat 20867 basis2 20976 tg2 20990 clsndisj 21100 cnpimaex 21281 t1sncld 21351 regsep 21359 nrmsep3 21380 cmpsub 21424 2ndc1stc 21475 refssex 21535 ptfinfin 21543 txcnpi 21632 txcmplem1 21665 tx1stc 21674 filss 21877 ufilss 21929 fclsopni 22039 fclsrest 22048 alexsubb 22070 alexsubALTlem2 22072 alexsubALTlem4 22074 ghmcnp 22138 qustgplem 22144 mopni 22517 metrest 22549 metcnpi 22569 metcnpi2 22570 nmolb 22741 nmoleub2lem2 23135 ovoliunlem1 23490 ovolicc2lem3 23507 mblsplit 23520 fta1b 24149 plycj 24253 lgamgulmlem1 24976 sqfpc 25084 ostth2lem2 25544 ostth3 25548 nbgrnself2OLD 26482 vdiscusgr 26662 rusgrnumwrdl2 26717 ewlkinedg 26735 numclwwlk1 27548 l2p 27673 lpni 27674 nvz 27864 chcompl 28439 ocin 28495 hmopidmchi 29350 dmdmd 29499 dmdbr5 29507 mdsl1i 29520 sigaclci 30535 bnj23 31124 kur14lem9 31534 sconnpht 31549 cvmsdisj 31590 untelirr 31923 untsucf 31925 dfon2lem4 32027 dfon2lem6 32029 dfon2lem7 32030 dfon2lem8 32031 dfon2 32033 frrlem5e 32125 sltval2 32146 fwddifnp1 32609 poimirlem18 33760 poimirlem21 33763 heibor1lem 33940 heiborlem4 33945 heiborlem6 33947 atlex 35125 psubspi 35555 elpcliN 35701 ldilval 35921 trlord 36378 tendotp 36570 hdmapval2 37642 pwelg 38391 gneispace0nelrn2 38965 gneispaceel2 38968 gneispacess2 38970 stoweid 40797 iccpartltu 41889 iccpartgtl 41890 iccpartleu 41892 iccpartgel 41893 |
Copyright terms: Public domain | W3C validator |