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 3575 | . 2 ⊢ (𝐴 ∈ 𝐵 → (∀𝑥 ∈ 𝐵 𝜑 → 𝜓)) |
3 | 2 | com12 32 | 1 ⊢ (∀𝑥 ∈ 𝐵 𝜑 → (𝐴 ∈ 𝐵 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 = wceq 1541 ∈ wcel 2106 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 |
This theorem depends on definitions: df-bi 206 df-an 397 df-tru 1544 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3063 |
This theorem is referenced by: elinti 4914 trss 5231 fvn0ssdmfun 7022 dff3 7046 2fvcoidd 7239 ofrval 7625 limsuc 7781 limuni3 7784 peano5 7826 frxp 8054 wfrdmclOLD 8259 smo11 8306 odi 8522 supub 9391 suplub 9392 elirrv 9528 dfom3 9579 noinfep 9592 tcrank 9816 alephle 10020 dfac5lem5 10059 dfac2b 10062 cofsmo 10201 coftr 10205 infpssrlem4 10238 isf34lem6 10312 axcc2lem 10368 domtriomlem 10374 axdc2lem 10380 axdc3lem2 10383 axdc4lem 10387 ac5b 10410 zorn2lem2 10429 zorn2lem6 10433 pwcfsdom 10515 inar1 10707 grupw 10727 grupr 10729 gruurn 10730 grothpw 10758 grothpwex 10759 axgroth6 10760 grothomex 10761 nqereu 10861 supsrlem 11043 axpre-sup 11101 dedekind 11314 dedekindle 11315 supmullem1 12121 supmul 12123 peano5nni 12152 dfnn2 12162 peano5uzi 12588 zindd 12600 lcmfdvds 16510 lcmfunsn 16512 1arith 16791 ramcl 16893 clatleglb 18399 pslem 18453 cyccom 18987 psgndiflemA 20990 eqcoe1ply1eq 21652 mvmumamul1 21887 smadiadetlem0 21994 chpscmat 22175 basis2 22285 tg2 22299 clsndisj 22410 cnpimaex 22591 t1sncld 22661 regsep 22669 nrmsep3 22690 cmpsub 22735 2ndc1stc 22786 refssex 22846 ptfinfin 22854 txcnpi 22943 txcmplem1 22976 tx1stc 22985 filss 23188 ufilss 23240 fclsopni 23350 fclsrest 23359 alexsubb 23381 alexsubALTlem2 23383 alexsubALTlem4 23385 ghmcnp 23450 qustgplem 23456 mopni 23832 metrest 23864 metcnpi 23884 metcnpi2 23885 nmolb 24065 nmoleub2lem2 24463 ovoliunlem1 24850 ovolicc2lem3 24867 mblsplit 24880 fta1b 25518 plycj 25622 lgamgulmlem1 26362 sqfpc 26470 ostth2lem2 26966 ostth3 26970 sltval2 26988 nogt01o 27028 madebdayim 27201 madebdaylemlrcut 27212 vdiscusgr 28365 0vtxrusgr 28411 rusgrnumwrdl2 28420 ewlkinedg 28438 eupthseg 29036 upgreupthseg 29039 numclwwlk1 29191 l2p 29307 lpni 29308 nvz 29497 chcompl 30070 ocin 30124 hmopidmchi 30979 dmdmd 31128 dmdbr5 31136 mdsl1i 31149 sigaclci 32600 bnj23 33199 kur14lem9 33677 sconnpht 33692 cvmsdisj 33733 sat1el2xp 33842 untelirr 34148 untsucf 34150 dfon2lem4 34231 dfon2lem6 34233 dfon2lem7 34234 dfon2lem8 34235 dfon2 34237 fwddifnp1 34717 domalom 35842 pibt2 35855 poimirlem18 36063 poimirlem21 36066 heibor1lem 36235 heiborlem4 36240 heiborlem6 36242 atlex 37745 psubspi 38177 elpcliN 38323 ldilval 38543 trlord 38999 tendotp 39191 hdmapval2 40262 cantnfresb 41596 pwelg 41774 gneispace0nelrn2 42355 gneispaceel2 42358 gneispacess2 42360 stoweid 44236 iccpartimp 45541 iccpartltu 45549 iccpartgtl 45550 iccpartleu 45552 iccpartgel 45553 isomushgr 45950 isomuspgrlem1 45951 isomuspgr 45958 isomgrtrlem 45962 1arymaptf1 46660 |
Copyright terms: Public domain | W3C validator |