![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > rspc4v | Structured version Visualization version GIF version |
Description: 4-variable restricted specialization, using implicit substitution. (Contributed by Scott Fenton, 7-Feb-2025.) |
Ref | Expression |
---|---|
rspc4v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) |
rspc4v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) |
rspc4v.3 | ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) |
rspc4v.4 | ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜓)) |
Ref | Expression |
---|---|
rspc4v | ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-3an 1087 | . . 3 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ↔ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇)) | |
2 | rspc4v.1 | . . . . . 6 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
3 | 2 | ralbidv 3174 | . . . . 5 ⊢ (𝑥 = 𝐴 → (∀𝑤 ∈ 𝑈 𝜑 ↔ ∀𝑤 ∈ 𝑈 𝜒)) |
4 | rspc4v.2 | . . . . . 6 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
5 | 4 | ralbidv 3174 | . . . . 5 ⊢ (𝑦 = 𝐵 → (∀𝑤 ∈ 𝑈 𝜒 ↔ ∀𝑤 ∈ 𝑈 𝜃)) |
6 | rspc4v.3 | . . . . . 6 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜏)) | |
7 | 6 | ralbidv 3174 | . . . . 5 ⊢ (𝑧 = 𝐶 → (∀𝑤 ∈ 𝑈 𝜃 ↔ ∀𝑤 ∈ 𝑈 𝜏)) |
8 | 3, 5, 7 | rspc3v 3625 | . . . 4 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → ∀𝑤 ∈ 𝑈 𝜏)) |
9 | rspc4v.4 | . . . . 5 ⊢ (𝑤 = 𝐷 → (𝜏 ↔ 𝜓)) | |
10 | 9 | rspcv 3605 | . . . 4 ⊢ (𝐷 ∈ 𝑈 → (∀𝑤 ∈ 𝑈 𝜏 → 𝜓)) |
11 | 8, 10 | sylan9 507 | . . 3 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝐷 ∈ 𝑈) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓)) |
12 | 1, 11 | sylanbr 581 | . 2 ⊢ ((((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ 𝐶 ∈ 𝑇) ∧ 𝐷 ∈ 𝑈) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓)) |
13 | 12 | anasss 466 | 1 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆) ∧ (𝐶 ∈ 𝑇 ∧ 𝐷 ∈ 𝑈)) → (∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑆 ∀𝑧 ∈ 𝑇 ∀𝑤 ∈ 𝑈 𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ↔ wb 205 ∧ wa 395 ∧ w3a 1085 = wceq 1534 ∈ wcel 2099 ∀wral 3058 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2699 |
This theorem depends on definitions: df-bi 206 df-an 396 df-3an 1087 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2706 df-cleq 2720 df-clel 2806 df-ral 3059 |
This theorem is referenced by: rspc6v 3629 rspc8v 3630 |
Copyright terms: Public domain | W3C validator |