| 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 3178 | . . 3 ⊢ (𝑥 = 𝐴 → (∀𝑦 ∈ 𝐷 𝜑 ↔ ∀𝑦 ∈ 𝐷 𝜒)) |
| 3 | 2 | rspcv 3618 | . 2 ⊢ (𝐴 ∈ 𝐶 → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → ∀𝑦 ∈ 𝐷 𝜒)) |
| 4 | rspc2v.2 | . . 3 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜓)) | |
| 5 | 4 | rspcv 3618 | . 2 ⊢ (𝐵 ∈ 𝐷 → (∀𝑦 ∈ 𝐷 𝜒 → 𝜓)) |
| 6 | 3, 5 | sylan9 507 | 1 ⊢ ((𝐴 ∈ 𝐶 ∧ 𝐵 ∈ 𝐷) → (∀𝑥 ∈ 𝐶 ∀𝑦 ∈ 𝐷 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = 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: rspc2va 3634 rspc3v 3638 rspc6v 3643 disji2 5127 f1veqaeq 7277 isorel 7346 isosolem 7367 oveqrspc2v 7458 fovcld 7560 caovclg 7625 caovcomg 7628 caofidlcan 7735 resf1extb 7956 smoel 8400 fiint 9366 fiintOLD 9367 dffi3 9471 ltordlem 11788 seqhomo 14090 cshf1 14848 climcn2 15629 drsdir 18348 tsrlin 18630 dirge 18648 mgmhmlin 18712 issubmgm2 18716 mhmlin 18806 issubg2 19159 nsgbi 19175 ghmlin 19239 efgi 19737 efgred 19766 rglcom4d 20208 irredmul 20429 issubrng2 20558 issubrg2 20592 abvmul 20822 abvtri 20823 lmodlema 20863 islmodd 20864 rmodislmodlem 20927 rmodislmod 20928 lmhmlin 21034 lbsind 21079 rnglidlmcl 21226 ipcj 21652 obsip 21741 mplcoe5lem 22057 matecl 22431 dmatelnd 22502 scmateALT 22518 mdetdiaglem 22604 mdetdiagid 22606 pmatcoe1fsupp 22707 m2cpminvid2lem 22760 inopn 22905 basis1 22957 basis2 22958 iscldtop 23103 hausnei 23336 t1sep2 23377 nconnsubb 23431 r0sep 23756 fbasssin 23844 fcfneii 24045 ustssel 24214 xmeteq0 24348 tngngp3 24677 nmvs 24697 cncfi 24920 c1lip1 26036 aalioulem3 26376 logltb 26642 cvxcl 27028 2sqlem8 27470 nocvxminlem 27822 madebday 27938 negsproplem1 28060 negsprop 28067 axtgcgrrflx 28470 axtgsegcon 28472 axtg5seg 28473 axtgbtwnid 28474 axtgpasch 28475 axtgcont1 28476 axtgupdim2 28479 axtgeucl 28480 isperp2d 28724 f1otrgds 28877 brbtwn2 28920 axcontlem3 28981 axcontlem9 28987 axcontlem10 28988 upgrwlkdvdelem 29756 conngrv2edg 30214 frgrwopreglem5ALT 30341 ablocom 30567 nvs 30682 nvtri 30689 phpar2 30842 phpar 30843 shaddcl 31236 shmulcl 31237 cnopc 31932 unop 31934 hmop 31941 cnfnc 31949 adj1 31952 hstel2 32238 stj 32254 stcltr1i 32293 mddmdin0i 32450 cdj3lem1 32453 cdj3lem2b 32456 disji2f 32590 disjif2 32594 disjxpin 32601 isoun 32711 archirng 33195 archiexdiv 33197 slmdlema 33209 inelcarsg 34313 sibfof 34342 breprexplema 34645 axtgupdim2ALTV 34683 pconncn 35229 ivthALT 36336 poimirlem32 37659 ismtycnv 37809 ismtyima 37810 ismtyres 37815 bfplem1 37829 bfplem2 37830 ghomlinOLD 37895 rngohomadd 37976 rngohommul 37977 crngocom 38008 idladdcl 38026 idllmulcl 38027 idlrmulcl 38028 pridl 38044 ispridlc 38077 pridlc 38078 dmnnzd 38082 oposlem 39183 omllaw 39244 hlsuprexch 39383 lautle 40086 ltrnu 40123 tendovalco 40767 sticksstones1 42147 sticksstones2 42148 ntrkbimka 44051 relprel 44972 mullimc 45631 mullimcf 45638 lptre2pt 45655 fourierdlem54 46175 fcoresf1 47081 faovcl 47212 icceuelpartlem 47422 iccpartnel 47425 fargshiftf1 47428 sprsymrelfolem2 47480 reuopreuprim 47513 isubgr3stgrlem6 47938 isthincd2lem2 49084 |
| Copyright terms: Public domain | W3C validator |