| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > rspc3v | Structured version Visualization version GIF version | ||
| Description: 3-variable restricted specialization, using implicit substitution. (Contributed by NM, 10-May-2005.) |
| Ref | Expression |
|---|---|
| rspc3v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
| rspc3v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) |
| rspc3v.3 | ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) |
| Ref | Expression |
|---|---|
| rspc3v | ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | rspc3v.1 | . . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 2 | 1 | ralbidv 3178 | . . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑇 𝜑 ↔ ∀𝑧 ∈ 𝑇 𝜒)) |
| 3 | rspc3v.2 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
| 4 | 3 | ralbidv 3178 | . . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝑇 𝜒 ↔ ∀𝑧 ∈ 𝑇 𝜃)) |
| 5 | 2, 4 | rspc2v 3633 | . . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → ∀𝑧 ∈ 𝑇 𝜃)) |
| 6 | rspc3v.3 | . . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | |
| 7 | 6 | rspcv 3618 | . . 3 ⊢ (𝐶 ∈ 𝑇 → (∀𝑧 ∈ 𝑇 𝜃 → 𝜓)) |
| 8 | 5, 7 | sylan9 507 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
| 9 | 8 | 3impa 1110 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = 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-3an 1089 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: rspc3dv 3641 rspc4v 3642 pocl 5600 swopolem 5602 isopolem 7365 caovassg 7631 caovcang 7634 caovordig 7638 caovordg 7640 caovdig 7647 caovdirg 7650 caofass 7737 caoftrn 7738 frpoins3xp3g 8166 prslem 18343 posi 18363 latdisdlem 18541 dlatmjdi 18568 sgrpass 18738 gaass 19315 rngdi 20157 rngdir 20158 o2timesd 20207 rglcom4d 20208 islmodd 20864 rmodislmodlem 20927 rmodislmod 20928 lsscl 20940 assalem 21877 psmettri2 24319 xmettri2 24350 addsproplem1 28002 addsprop 28009 axtgcgrid 28471 axtg5seg 28473 axtgpasch 28475 axtgupdim2 28479 axtgeucl 28480 tgdim01 28515 f1otrgitv 28878 grpoass 30522 vcdi 30584 vcdir 30585 vcass 30586 lnolin 30773 lnopl 31933 lnfnl 31950 omndadd 33083 axtgupdim2ALTV 34683 rngodi 37911 rngodir 37912 rngoass 37913 lfli 39062 cvlexch1 39329 isthincd2lem2 49084 |
| Copyright terms: Public domain | W3C validator |