![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc2v | Structured version Visualization version GIF version |
Description: 2-variable restricted specialization, using implicit substitution. (Contributed by NM, 13-Sep-1999.) |
Ref | Expression |
---|---|
rspc2v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
rspc2v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc2v | ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rspc2v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
2 | 1 | ralbidv 3168 | . . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒)) |
3 | 2 | rspcv 3605 | . 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒)) |
4 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
5 | 4 | rspcv 3605 | . 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓)) |
6 | 3, 5 | sylan9 506 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2099 ∀wral 3051 |
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 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-ral 3052 |
This theorem is referenced by: rspc2va 3621 rspc3v 3625 rspc6v 3629 disji2 5129 f1veqaeq 7263 isorel 7329 isosolem 7350 oveqrspc2v 7442 fovcld 7544 caovclg 7609 caovcomg 7612 smoel 8381 fiint 9360 fiintOLD 9361 dffi3 9466 ltordlem 11779 seqhomo 14062 cshf1 14812 climcn2 15589 drsdir 18321 tsrlin 18604 dirge 18622 mgmhmlin 18686 issubmgm2 18690 mhmlin 18777 issubg2 19130 nsgbi 19146 ghmlin 19210 efgi 19712 efgred 19741 rglcom4d 20189 irredmul 20406 issubrng2 20535 issubrg2 20571 abvmul 20795 abvtri 20796 lmodlema 20836 islmodd 20837 rmodislmodlem 20900 rmodislmod 20901 rmodislmodOLD 20902 lmhmlin 21008 lbsind 21053 rnglidlmcl 21200 ipcj 21625 obsip 21714 mplcoe5lem 22041 matecl 22414 dmatelnd 22485 scmateALT 22501 mdetdiaglem 22587 mdetdiagid 22589 pmatcoe1fsupp 22690 m2cpminvid2lem 22743 inopn 22888 basis1 22940 basis2 22941 iscldtop 23086 hausnei 23319 t1sep2 23360 nconnsubb 23414 r0sep 23739 fbasssin 23827 fcfneii 24028 ustssel 24197 xmeteq0 24331 tngngp3 24660 nmvs 24680 cncfi 24901 c1lip1 26017 aalioulem3 26358 logltb 26623 cvxcl 27009 2sqlem8 27451 nocvxminlem 27803 madebday 27919 negsproplem1 28033 negsprop 28040 axtgcgrrflx 28385 axtgsegcon 28387 axtg5seg 28388 axtgbtwnid 28389 axtgpasch 28390 axtgcont1 28391 axtgupdim2 28394 axtgeucl 28395 isperp2d 28639 f1otrgds 28792 brbtwn2 28835 axcontlem3 28896 axcontlem9 28902 axcontlem10 28903 upgrwlkdvdelem 29669 conngrv2edg 30124 frgrwopreglem5ALT 30251 ablocom 30477 nvs 30592 nvtri 30599 phpar2 30752 phpar 30753 shaddcl 31146 shmulcl 31147 cnopc 31842 unop 31844 hmop 31851 cnfnc 31859 adj1 31862 hstel2 32148 stj 32164 stcltr1i 32203 mddmdin0i 32360 cdj3lem1 32363 cdj3lem2b 32366 disji2f 32496 disjif2 32500 disjxpin 32507 isoun 32612 archirng 33056 archiexdiv 33058 slmdlema 33070 inelcarsg 34157 sibfof 34186 breprexplema 34488 axtgupdim2ALTV 34526 pconncn 35064 ivthALT 36059 poimirlem32 37365 ismtycnv 37515 ismtyima 37516 ismtyres 37521 bfplem1 37535 bfplem2 37536 ghomlinOLD 37601 rngohomadd 37682 rngohommul 37683 crngocom 37714 idladdcl 37732 idllmulcl 37733 idlrmulcl 37734 pridl 37750 ispridlc 37783 pridlc 37784 dmnnzd 37788 oposlem 38892 omllaw 38953 hlsuprexch 39092 lautle 39795 ltrnu 39832 tendovalco 40476 sticksstones1 41857 sticksstones2 41858 ntrkbimka 43741 mullimc 45272 mullimcf 45279 lptre2pt 45296 fourierdlem54 45816 fcoresf1 46719 faovcl 46848 icceuelpartlem 47042 iccpartnel 47045 fargshiftf1 47048 sprsymrelfolem2 47100 reuopreuprim 47133 isthincd2lem2 48392 |
Copyright terms: Public domain | W3C validator |