| 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 3618 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
| 3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 = wceq 1540 ∈ wcel 2108 ∀wral 3061 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ral 3062 |
| This theorem is referenced by: elinti 4955 trss 5270 fvn0ssdmfun 7094 dff3 7120 2fvcoidd 7317 ofrval 7709 limsuc 7870 limuni3 7873 peano5 7915 frxp 8151 wfrdmclOLD 8357 smo11 8404 odi 8617 supub 9499 suplub 9500 elirrv 9636 dfom3 9687 noinfep 9700 tcrank 9924 alephle 10128 dfac5lem5 10167 dfac2b 10171 cofsmo 10309 coftr 10313 infpssrlem4 10346 isf34lem6 10420 axcc2lem 10476 domtriomlem 10482 axdc2lem 10488 axdc3lem2 10491 axdc4lem 10495 ac5b 10518 zorn2lem2 10537 zorn2lem6 10541 pwcfsdom 10623 inar1 10815 grupw 10835 grupr 10837 gruurn 10838 grothpw 10866 grothpwex 10867 axgroth6 10868 grothomex 10869 nqereu 10969 supsrlem 11151 axpre-sup 11209 dedekind 11424 dedekindle 11425 supmullem1 12238 supmul 12240 peano5nni 12269 dfnn2 12279 peano5uzi 12707 zindd 12719 lcmfdvds 16679 lcmfunsn 16681 1arith 16965 ramcl 17067 clatleglb 18563 pslem 18617 cyccom 19221 rngisomring1 20468 psgndiflemA 21619 eqcoe1ply1eq 22303 mvmumamul1 22560 smadiadetlem0 22667 chpscmat 22848 basis2 22958 tg2 22972 clsndisj 23083 cnpimaex 23264 t1sncld 23334 regsep 23342 nrmsep3 23363 cmpsub 23408 2ndc1stc 23459 refssex 23519 ptfinfin 23527 txcnpi 23616 txcmplem1 23649 tx1stc 23658 filss 23861 ufilss 23913 fclsopni 24023 fclsrest 24032 alexsubb 24054 alexsubALTlem2 24056 alexsubALTlem4 24058 ghmcnp 24123 qustgplem 24129 mopni 24505 metrest 24537 metcnpi 24557 metcnpi2 24558 nmolb 24738 nmoleub2lem2 25149 ovoliunlem1 25537 ovolicc2lem3 25554 mblsplit 25567 fta1b 26211 plycj 26317 plycjOLD 26319 lgamgulmlem1 27072 sqfpc 27180 ostth2lem2 27678 ostth3 27682 sltval2 27701 nogt01o 27741 madebdayim 27926 madebdaylemlrcut 27937 precsexlem9 28239 dfn0s2 28336 peano5uzs 28390 vdiscusgr 29549 0vtxrusgr 29595 rusgrnumwrdl2 29604 ewlkinedg 29622 eupthseg 30225 upgreupthseg 30228 numclwwlk1 30380 l2p 30498 lpni 30499 nvz 30688 chcompl 31261 ocin 31315 hmopidmchi 32170 dmdmd 32319 dmdbr5 32327 mdsl1i 32340 sigaclci 34133 bnj23 34732 kur14lem9 35219 sconnpht 35234 cvmsdisj 35275 sat1el2xp 35384 untelirr 35708 untsucf 35710 dfon2lem4 35787 dfon2lem6 35789 dfon2lem7 35790 dfon2lem8 35791 dfon2 35793 fwddifnp1 36166 domalom 37405 pibt2 37418 poimirlem18 37645 poimirlem21 37648 heibor1lem 37816 heiborlem4 37821 heiborlem6 37823 atlex 39317 psubspi 39749 elpcliN 39895 ldilval 40115 trlord 40571 tendotp 40763 hdmapval2 41834 cantnfresb 43337 pwelg 43573 gneispace0nelrn2 44154 gneispaceel2 44157 gneispacess2 44159 stoweid 46078 iccpartimp 47404 iccpartltu 47412 iccpartgtl 47413 iccpartleu 47415 iccpartgel 47416 isuspgrim0 47872 gricushgr 47886 1arymaptf1 48563 |
| Copyright terms: Public domain | W3C validator |