![]() |
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 3167 | . . . 4 ⊢ (𝑥 = 𝐴 → (∀𝑧 ∈ 𝑇 𝜑 ↔ ∀𝑧 ∈ 𝑇 𝜒)) |
3 | rspc3v.2 | . . . . 5 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
4 | 3 | ralbidv 3167 | . . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑧 ∈ 𝑇 𝜒 ↔ ∀𝑧 ∈ 𝑇 𝜃)) |
5 | 2, 4 | rspc2v 3617 | . . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → ∀𝑧 ∈ 𝑇 𝜃)) |
6 | rspc3v.3 | . . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | |
7 | 6 | rspcv 3602 | . . 3 ⊢ (𝐶 ∈ 𝑇 → (∀𝑧 ∈ 𝑇 𝜃 → 𝜓)) |
8 | 5, 7 | sylan9 506 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
9 | 8 | 3impa 1107 | 1 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∧ w3a 1084 = wceq 1533 ∈ wcel 2098 ∀wral 3050 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1789 ax-4 1803 ax-5 1905 ax-6 1963 ax-7 2003 ax-8 2100 ax-9 2108 ax-ext 2696 |
This theorem depends on definitions: df-bi 206 df-an 395 df-3an 1086 df-tru 1536 df-ex 1774 df-sb 2060 df-clab 2703 df-cleq 2717 df-clel 2802 df-ral 3051 |
This theorem is referenced by: rspc3dv 3624 rspc4v 3625 pocl 5597 swopolem 5600 isopolem 7352 caovassg 7619 caovcang 7622 caovordig 7626 caovordg 7628 caovdig 7635 caovdirg 7638 caofass 7723 caoftrn 7724 frpoins3xp3g 8146 prslem 18293 posi 18312 latdisdlem 18491 dlatmjdi 18518 sgrpass 18688 gaass 19260 rngdi 20112 rngdir 20113 o2timesd 20162 rglcom4d 20163 islmodd 20761 rmodislmodlem 20824 rmodislmod 20825 rmodislmodOLD 20826 lsscl 20838 assalem 21808 psmettri2 24259 xmettri2 24290 addsproplem1 27932 addsprop 27939 axtgcgrid 28339 axtg5seg 28341 axtgpasch 28343 axtgupdim2 28347 axtgeucl 28348 tgdim01 28383 f1otrgitv 28746 grpoass 30385 vcdi 30447 vcdir 30448 vcass 30449 lnolin 30636 lnopl 31796 lnfnl 31813 omndadd 32876 axtgupdim2ALTV 34431 rngodi 37508 rngodir 37509 rngoass 37510 lfli 38663 cvlexch1 38930 isthincd2lem2 48228 |
Copyright terms: Public domain | W3C validator |