![]() |
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 3623 | . . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → ∀𝑧 ∈ 𝑇 𝜃)) |
6 | rspc3v.3 | . . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | |
7 | 6 | rspcv 3609 | . . 3 ⊢ (𝐶 ∈ 𝑇 → (∀𝑧 ∈ 𝑇 𝜃 → 𝜓)) |
8 | 5, 7 | sylan9 509 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
9 | 8 | 3impa 1111 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 397 ∧ w3a 1088 = wceq 1542 ∈ wcel 2107 ∀wral 3062 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-ext 2704 |
This theorem depends on definitions: df-bi 206 df-an 398 df-3an 1090 df-tru 1545 df-ex 1783 df-sb 2069 df-clab 2711 df-cleq 2725 df-clel 2811 df-ral 3063 |
This theorem is referenced by: rspc3dv 3630 rspc4v 3631 pocl 5596 swopolem 5599 isopolem 7342 caovassg 7605 caovcang 7608 caovordig 7612 caovordg 7614 caovdig 7621 caovdirg 7624 caofass 7707 caoftrn 7708 frpoins3xp3g 8127 prslem 18251 posi 18270 latdisdlem 18449 dlatmjdi 18476 sgrpass 18616 gaass 19161 o2timesd 20033 rglcom4d 20034 islmodd 20477 rmodislmodlem 20539 rmodislmod 20540 rmodislmodOLD 20541 lsscl 20553 assalem 21412 psmettri2 23815 xmettri2 23846 addsproplem1 27455 addsprop 27462 axtgcgrid 27745 axtg5seg 27747 axtgpasch 27749 axtgupdim2 27753 axtgeucl 27754 tgdim01 27789 f1otrgitv 28152 grpoass 29787 vcdi 29849 vcdir 29850 vcass 29851 lnolin 30038 lnopl 31198 lnfnl 31215 omndadd 32255 axtgupdim2ALTV 33711 rngodi 36820 rngodir 36821 rngoass 36822 lfli 37979 cvlexch1 38246 rngdi 46707 rngdir 46708 isthincd2lem2 47704 |
Copyright terms: Public domain | W3C validator |