Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > rgen2a | Unicode version |
Description: Generalization rule for restricted quantification. Note that and are not required to be disjoint. This proof illustrates the use of dvelim 1997. Usage of rgen2 2543 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 1508 | . . . . 5 | |
2 | eleq1 2220 | . . . . 5 | |
3 | 1, 2 | dvelimor 1998 | . . . 4 |
4 | eleq1 2220 | . . . . . . . . 9 | |
5 | rgen2a.1 | . . . . . . . . . 10 | |
6 | 5 | ex 114 | . . . . . . . . 9 |
7 | 4, 6 | syl6bi 162 | . . . . . . . 8 |
8 | 7 | pm2.43d 50 | . . . . . . 7 |
9 | 8 | alimi 1435 | . . . . . 6 |
10 | 9 | a1d 22 | . . . . 5 |
11 | nfr 1498 | . . . . . 6 | |
12 | 6 | alimi 1435 | . . . . . 6 |
13 | 11, 12 | syl6 33 | . . . . 5 |
14 | 10, 13 | jaoi 706 | . . . 4 |
15 | 3, 14 | ax-mp 5 | . . 3 |
16 | df-ral 2440 | . . 3 | |
17 | 15, 16 | sylibr 133 | . 2 |
18 | 17 | rgen 2510 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 103 wo 698 wal 1333 wceq 1335 wnf 1440 wcel 2128 wral 2435 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-io 699 ax-5 1427 ax-7 1428 ax-gen 1429 ax-ie1 1473 ax-ie2 1474 ax-8 1484 ax-10 1485 ax-11 1486 ax-i12 1487 ax-bndl 1489 ax-4 1490 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2139 |
This theorem depends on definitions: df-bi 116 df-nf 1441 df-sb 1743 df-cleq 2150 df-clel 2153 df-ral 2440 |
This theorem is referenced by: ordsucunielexmid 4492 onintexmid 4534 isoid 5762 issmo 6237 oawordriexmid 6419 ecopover 6580 ecopoverg 6583 1domsn 6766 unfiexmid 6864 axaddf 7790 axmulf 7791 subf 8081 negiso 8831 cnref1o 9565 xaddf 9754 ioof 9881 fzof 10052 xrnegiso 11170 reeff1 11608 gcdf 11871 eucalgf 11947 qredeu 11989 qnnen 12230 strsetsid 12293 hmeofn 12772 ismeti 12816 qtopbasss 12991 tgqioo 13017 peano4nninf 13649 |
Copyright terms: Public domain | W3C validator |