![]() |
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 3176 | . . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑇 𝜑 ↔ ∀𝑧 ∈ 𝑇 𝜒)) |
3 | rspc3v.2 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
4 | 3 | ralbidv 3176 | . . . 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 1109 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1537 ∈ wcel 2106 ∀wral 3059 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1792 ax-4 1806 ax-5 1908 ax-6 1965 ax-7 2005 ax-8 2108 ax-9 2116 ax-ext 2706 |
This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1540 df-ex 1777 df-sb 2063 df-clab 2713 df-cleq 2727 df-clel 2814 df-ral 3060 |
This theorem is referenced by: rspc3dv 3641 rspc4v 3642 pocl 5605 swopolem 5607 isopolem 7365 caovassg 7631 caovcang 7634 caovordig 7638 caovordg 7640 caovdig 7647 caovdirg 7650 caofass 7736 caoftrn 7737 frpoins3xp3g 8165 prslem 18355 posi 18375 latdisdlem 18554 dlatmjdi 18581 sgrpass 18751 gaass 19328 rngdi 20178 rngdir 20179 o2timesd 20228 rglcom4d 20229 islmodd 20881 rmodislmodlem 20944 rmodislmod 20945 rmodislmodOLD 20946 lsscl 20958 assalem 21895 psmettri2 24335 xmettri2 24366 addsproplem1 28017 addsprop 28024 axtgcgrid 28486 axtg5seg 28488 axtgpasch 28490 axtgupdim2 28494 axtgeucl 28495 tgdim01 28530 f1otrgitv 28893 grpoass 30532 vcdi 30594 vcdir 30595 vcass 30596 lnolin 30783 lnopl 31943 lnfnl 31960 omndadd 33066 axtgupdim2ALTV 34662 rngodi 37891 rngodir 37892 rngoass 37893 lfli 39043 cvlexch1 39310 isthincd2lem2 48836 |
Copyright terms: Public domain | W3C validator |