Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > opelopabsb | Unicode version |
Description: The law of concretion in terms of substitutions. (Contributed by NM, 30-Sep-2002.) (Revised by Mario Carneiro, 18-Nov-2016.) |
Ref | Expression |
---|---|
opelopabsb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elopab 4180 | . . . 4 | |
2 | simpl 108 | . . . . . . . 8 | |
3 | 2 | eqcomd 2145 | . . . . . . 7 |
4 | vex 2689 | . . . . . . . 8 | |
5 | vex 2689 | . . . . . . . 8 | |
6 | 4, 5 | opth 4159 | . . . . . . 7 |
7 | 3, 6 | sylib 121 | . . . . . 6 |
8 | 7 | 2eximi 1580 | . . . . 5 |
9 | eeanv 1904 | . . . . . 6 | |
10 | isset 2692 | . . . . . . 7 | |
11 | isset 2692 | . . . . . . 7 | |
12 | 10, 11 | anbi12i 455 | . . . . . 6 |
13 | 9, 12 | bitr4i 186 | . . . . 5 |
14 | 8, 13 | sylib 121 | . . . 4 |
15 | 1, 14 | sylbi 120 | . . 3 |
16 | nfv 1508 | . . . 4 | |
17 | nfv 1508 | . . . 4 | |
18 | nfs1v 1912 | . . . 4 | |
19 | nfs1v 1912 | . . . . 5 | |
20 | 19 | nfsbxy 1915 | . . . 4 |
21 | sbequ12 1744 | . . . . 5 | |
22 | sbequ12 1744 | . . . . 5 | |
23 | 21, 22 | sylan9bbr 458 | . . . 4 |
24 | 16, 17, 18, 20, 23 | cbvopab 3999 | . . 3 |
25 | 15, 24 | eleq2s 2234 | . 2 |
26 | sbcex 2917 | . . 3 | |
27 | spesbc 2994 | . . . 4 | |
28 | sbcex 2917 | . . . . 5 | |
29 | 28 | exlimiv 1577 | . . . 4 |
30 | 27, 29 | syl 14 | . . 3 |
31 | 26, 30 | jca 304 | . 2 |
32 | opeq1 3705 | . . . . 5 | |
33 | 32 | eleq1d 2208 | . . . 4 |
34 | dfsbcq2 2912 | . . . 4 | |
35 | 33, 34 | bibi12d 234 | . . 3 |
36 | opeq2 3706 | . . . . 5 | |
37 | 36 | eleq1d 2208 | . . . 4 |
38 | dfsbcq2 2912 | . . . . 5 | |
39 | 38 | sbcbidv 2967 | . . . 4 |
40 | 37, 39 | bibi12d 234 | . . 3 |
41 | nfopab1 3997 | . . . . . 6 | |
42 | 41 | nfel2 2294 | . . . . 5 |
43 | nfs1v 1912 | . . . . 5 | |
44 | 42, 43 | nfbi 1568 | . . . 4 |
45 | opeq1 3705 | . . . . . 6 | |
46 | 45 | eleq1d 2208 | . . . . 5 |
47 | sbequ12 1744 | . . . . 5 | |
48 | 46, 47 | bibi12d 234 | . . . 4 |
49 | nfopab2 3998 | . . . . . . 7 | |
50 | 49 | nfel2 2294 | . . . . . 6 |
51 | nfs1v 1912 | . . . . . 6 | |
52 | 50, 51 | nfbi 1568 | . . . . 5 |
53 | opeq2 3706 | . . . . . . 7 | |
54 | 53 | eleq1d 2208 | . . . . . 6 |
55 | sbequ12 1744 | . . . . . 6 | |
56 | 54, 55 | bibi12d 234 | . . . . 5 |
57 | opabid 4179 | . . . . 5 | |
58 | 52, 56, 57 | chvar 1730 | . . . 4 |
59 | 44, 48, 58 | chvar 1730 | . . 3 |
60 | 35, 40, 59 | vtocl2g 2750 | . 2 |
61 | 25, 31, 60 | pm5.21nii 693 | 1 |
Colors of variables: wff set class |
Syntax hints: wa 103 wb 104 wceq 1331 wex 1468 wcel 1480 wsb 1735 cvv 2686 wsbc 2909 cop 3530 copab 3988 |
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 698 ax-5 1423 ax-7 1424 ax-gen 1425 ax-ie1 1469 ax-ie2 1470 ax-8 1482 ax-10 1483 ax-11 1484 ax-i12 1485 ax-bndl 1486 ax-4 1487 ax-14 1492 ax-17 1506 ax-i9 1510 ax-ial 1514 ax-i5r 1515 ax-ext 2121 ax-sep 4046 ax-pow 4098 ax-pr 4131 |
This theorem depends on definitions: df-bi 116 df-3an 964 df-tru 1334 df-nf 1437 df-sb 1736 df-eu 2002 df-mo 2003 df-clab 2126 df-cleq 2132 df-clel 2135 df-nfc 2270 df-rex 2422 df-v 2688 df-sbc 2910 df-un 3075 df-in 3077 df-ss 3084 df-pw 3512 df-sn 3533 df-pr 3534 df-op 3536 df-opab 3990 |
This theorem is referenced by: brabsb 4183 opelopabaf 4195 opelopabf 4196 difopab 4672 isarep1 5209 |
Copyright terms: Public domain | W3C validator |