|   | Metamath Proof Explorer | < Previous  
      Next > Nearby theorems | |
| Mirrors > Home > MPE Home > Th. List > rspc3ev | Structured version Visualization version GIF version | ||
| Description: 3-variable restricted existential specialization, using implicit substitution. (Contributed by NM, 25-Jul-2012.) | 
| Ref | Expression | 
|---|---|
| rspc3v.1 | ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | 
| rspc3v.2 | ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | 
| rspc3v.3 | ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | 
| Ref | Expression | 
|---|---|
| rspc3ev | ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) | 
| Step | Hyp | Ref | Expression | 
|---|---|---|---|
| 1 | simpl1 1191 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐴 ∈ 𝑅) | |
| 2 | simpl2 1192 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → 𝐵 ∈ 𝑆) | |
| 3 | rspc3v.3 | . . . 4 ⊢ (𝑧 = 𝐶 → (𝜃 ↔ 𝜓)) | |
| 4 | 3 | rspcev 3621 | . . 3 ⊢ ((𝐶 ∈ 𝑇 ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃) | 
| 5 | 4 | 3ad2antl3 1187 | . 2 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑧 ∈ 𝑇 𝜃) | 
| 6 | rspc3v.1 | . . . 4 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜒)) | |
| 7 | 6 | rexbidv 3178 | . . 3 ⊢ (𝑥 = 𝐴 → (∃𝑧 ∈ 𝑇 𝜑 ↔ ∃𝑧 ∈ 𝑇 𝜒)) | 
| 8 | rspc3v.2 | . . . 4 ⊢ (𝑦 = 𝐵 → (𝜒 ↔ 𝜃)) | |
| 9 | 8 | rexbidv 3178 | . . 3 ⊢ (𝑦 = 𝐵 → (∃𝑧 ∈ 𝑇 𝜒 ↔ ∃𝑧 ∈ 𝑇 𝜃)) | 
| 10 | 7, 9 | rspc2ev 3634 | . 2 ⊢ ((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ ∃𝑧 ∈ 𝑇 𝜃) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) | 
| 11 | 1, 2, 5, 10 | syl3anc 1372 | 1 ⊢ (((𝐴 ∈ 𝑅 ∧ 𝐵 ∈ 𝑆 ∧ 𝐶 ∈ 𝑇) ∧ 𝜓) → ∃𝑥 ∈ 𝑅 ∃𝑦 ∈ 𝑆 ∃𝑧 ∈ 𝑇 𝜑) | 
| Colors of variables: wff setvar class | 
| Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1539 ∈ wcel 2107 ∃wrex 3069 | 
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-ext 2707 | 
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1088 df-tru 1542 df-ex 1779 df-sb 2064 df-clab 2714 df-cleq 2728 df-clel 2815 df-ral 3061 df-rex 3070 | 
| This theorem is referenced by: 3rspcedvdw 3639 f1dom3el3dif 7290 wrdl3s3 15002 pmltpclem1 25484 axlowdim 28977 axeuclidlem 28978 upgr3v3e3cycl 30200 br8d 32623 tgoldbachgt 34679 2goelgoanfmla1 35430 br8 35757 br6 35758 3dim1lem5 39469 lplni2 39540 3cubes 42706 jm2.27 43025 grimgrtri 47921 usgrexmpl1tri 47989 | 
| Copyright terms: Public domain | W3C validator |