![]() |
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 3603 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1534 ∈ wcel 2099 ∀wral 3056 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2698 |
This theorem depends on definitions: df-bi 206 df-an 396 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2705 df-cleq 2719 df-clel 2805 df-ral 3057 |
This theorem is referenced by: elinti 4953 trss 5270 fvn0ssdmfun 7078 dff3 7104 2fvcoidd 7300 ofrval 7691 limsuc 7847 limuni3 7850 peano5 7893 frxp 8125 wfrdmclOLD 8331 smo11 8378 odi 8593 supub 9474 suplub 9475 elirrv 9611 dfom3 9662 noinfep 9675 tcrank 9899 alephle 10103 dfac5lem5 10142 dfac2b 10145 cofsmo 10284 coftr 10288 infpssrlem4 10321 isf34lem6 10395 axcc2lem 10451 domtriomlem 10457 axdc2lem 10463 axdc3lem2 10466 axdc4lem 10470 ac5b 10493 zorn2lem2 10512 zorn2lem6 10516 pwcfsdom 10598 inar1 10790 grupw 10810 grupr 10812 gruurn 10813 grothpw 10841 grothpwex 10842 axgroth6 10843 grothomex 10844 nqereu 10944 supsrlem 11126 axpre-sup 11184 dedekind 11399 dedekindle 11400 supmullem1 12206 supmul 12208 peano5nni 12237 dfnn2 12247 peano5uzi 12673 zindd 12685 lcmfdvds 16604 lcmfunsn 16606 1arith 16887 ramcl 16989 clatleglb 18501 pslem 18555 cyccom 19149 rngisomring1 20396 psgndiflemA 21520 eqcoe1ply1eq 22205 mvmumamul1 22443 smadiadetlem0 22550 chpscmat 22731 basis2 22841 tg2 22855 clsndisj 22966 cnpimaex 23147 t1sncld 23217 regsep 23225 nrmsep3 23246 cmpsub 23291 2ndc1stc 23342 refssex 23402 ptfinfin 23410 txcnpi 23499 txcmplem1 23532 tx1stc 23541 filss 23744 ufilss 23796 fclsopni 23906 fclsrest 23915 alexsubb 23937 alexsubALTlem2 23939 alexsubALTlem4 23941 ghmcnp 24006 qustgplem 24012 mopni 24388 metrest 24420 metcnpi 24440 metcnpi2 24441 nmolb 24621 nmoleub2lem2 25030 ovoliunlem1 25418 ovolicc2lem3 25435 mblsplit 25448 fta1b 26093 plycj 26199 lgamgulmlem1 26948 sqfpc 27056 ostth2lem2 27554 ostth3 27558 sltval2 27576 nogt01o 27616 madebdayim 27801 madebdaylemlrcut 27812 precsexlem9 28100 dfn0s2 28188 vdiscusgr 29332 0vtxrusgr 29378 rusgrnumwrdl2 29387 ewlkinedg 29405 eupthseg 30003 upgreupthseg 30006 numclwwlk1 30158 l2p 30276 lpni 30277 nvz 30466 chcompl 31039 ocin 31093 hmopidmchi 31948 dmdmd 32097 dmdbr5 32105 mdsl1i 32118 sigaclci 33687 bnj23 34285 kur14lem9 34760 sconnpht 34775 cvmsdisj 34816 sat1el2xp 34925 untelirr 35238 untsucf 35240 dfon2lem4 35318 dfon2lem6 35320 dfon2lem7 35321 dfon2lem8 35322 dfon2 35324 fwddifnp1 35697 domalom 36819 pibt2 36832 poimirlem18 37046 poimirlem21 37049 heibor1lem 37217 heiborlem4 37222 heiborlem6 37224 atlex 38725 psubspi 39157 elpcliN 39303 ldilval 39523 trlord 39979 tendotp 40171 hdmapval2 41242 cantnfresb 42676 pwelg 42913 gneispace0nelrn2 43494 gneispaceel2 43497 gneispacess2 43499 stoweid 45374 iccpartimp 46680 iccpartltu 46688 iccpartgtl 46689 iccpartleu 46691 iccpartgel 46692 isuspgrim0 47093 gricushgr 47106 1arymaptf1 47638 |
Copyright terms: Public domain | W3C validator |