![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > rgen2a | GIF version |
Description: Generalization rule for restricted quantification. Note that 𝑥 and 𝑦 are not required to be disjoint. This proof illustrates the use of dvelim 2029. Usage of rgen2 2576 instead is highly encouraged. (Contributed by NM, 23-Nov-1994.) (Proof rewritten by Jim Kingdon, 1-Jun-2018.) (New usage is discouraged.) |
Ref | Expression |
---|---|
rgen2a.1 | ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑) |
Ref | Expression |
---|---|
rgen2a | ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nfv 1539 | . . . . 5 ⊢ Ⅎ𝑦 𝑧 ∈ 𝐴 | |
2 | eleq1 2252 | . . . . 5 ⊢ (𝑧 = 𝑥 → (𝑧 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) | |
3 | 1, 2 | dvelimor 2030 | . . . 4 ⊢ (∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴) |
4 | eleq1 2252 | . . . . . . . . 9 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 ↔ 𝑥 ∈ 𝐴)) | |
5 | rgen2a.1 | . . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) → 𝜑) | |
6 | 5 | ex 115 | . . . . . . . . 9 ⊢ (𝑥 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑)) |
7 | 4, 6 | biimtrdi 163 | . . . . . . . 8 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → (𝑦 ∈ 𝐴 → 𝜑))) |
8 | 7 | pm2.43d 50 | . . . . . . 7 ⊢ (𝑦 = 𝑥 → (𝑦 ∈ 𝐴 → 𝜑)) |
9 | 8 | alimi 1466 | . . . . . 6 ⊢ (∀𝑦 𝑦 = 𝑥 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)) |
10 | 9 | a1d 22 | . . . . 5 ⊢ (∀𝑦 𝑦 = 𝑥 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))) |
11 | nfr 1529 | . . . . . 6 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦 𝑥 ∈ 𝐴)) | |
12 | 6 | alimi 1466 | . . . . . 6 ⊢ (∀𝑦 𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)) |
13 | 11, 12 | syl6 33 | . . . . 5 ⊢ (Ⅎ𝑦 𝑥 ∈ 𝐴 → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))) |
14 | 10, 13 | jaoi 717 | . . . 4 ⊢ ((∀𝑦 𝑦 = 𝑥 ∨ Ⅎ𝑦 𝑥 ∈ 𝐴) → (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑))) |
15 | 3, 14 | ax-mp 5 | . . 3 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)) |
16 | df-ral 2473 | . . 3 ⊢ (∀𝑦 ∈ 𝐴 𝜑 ↔ ∀𝑦(𝑦 ∈ 𝐴 → 𝜑)) | |
17 | 15, 16 | sylibr 134 | . 2 ⊢ (𝑥 ∈ 𝐴 → ∀𝑦 ∈ 𝐴 𝜑) |
18 | 17 | rgen 2543 | 1 ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 𝜑 |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ∨ wo 709 ∀wal 1362 = wceq 1364 Ⅎwnf 1471 ∈ wcel 2160 ∀wral 2468 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-io 710 ax-5 1458 ax-7 1459 ax-gen 1460 ax-ie1 1504 ax-ie2 1505 ax-8 1515 ax-10 1516 ax-11 1517 ax-i12 1518 ax-bndl 1520 ax-4 1521 ax-17 1537 ax-i9 1541 ax-ial 1545 ax-i5r 1546 ax-ext 2171 |
This theorem depends on definitions: df-bi 117 df-nf 1472 df-sb 1774 df-cleq 2182 df-clel 2185 df-ral 2473 |
This theorem is referenced by: ordsucunielexmid 4548 onintexmid 4590 isoid 5832 issmo 6314 oawordriexmid 6496 ecopover 6660 ecopoverg 6663 1domsn 6846 unfiexmid 6947 axaddf 7898 axmulf 7899 subf 8190 negiso 8943 cnref1o 9682 xaddf 9876 ioof 10003 fzof 10176 xrnegiso 11305 reeff1 11743 gcdf 12008 eucalgf 12090 qredeu 12132 qnnen 12485 strsetsid 12548 hmeofn 14279 ismeti 14323 qtopbasss 14498 tgqioo 14524 peano4nninf 15234 |
Copyright terms: Public domain | W3C validator |